%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : PRO007+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jul 23 06:14:06 EDT 2022
% Result : CounterSatisfiable 28.24s 28.40s
% Output : Model 28.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PRO007+3 : TPTP v8.1.0. Released v4.0.0.
% 0.00/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.12/0.33 % Computer : n004.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jul 22 13:27:51 EDT 2022
% 0.12/0.33 % CPUTime :
% 28.24/28.40 GeoParameters:
% 28.24/28.40
% 28.24/28.40 tptp_input = 1
% 28.24/28.40 tptp_output = 0
% 28.24/28.40 nonempty = 1
% 28.24/28.40 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.24/28.40 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 28.24/28.40
% 28.24/28.40
% 28.24/28.40 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.24/28.40 % SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.24/28.40
% 28.24/28.40 Interpretation 425:
% 28.24/28.40 Guesses:
% 28.24/28.40 0 : guesser 1, 0, ( | 1, 0 ), 0, 28s old, 0 lemmas
% 28.24/28.40 1 : guesser 3, 1, ( 1 | 2, 0 ), 0, 28s old, 1 lemmas
% 28.24/28.40 2 : guesser 5, 2, ( 2, 1 | 3, 0 ), 10, 28s old, 2 lemmas
% 28.24/28.40 3 : guesser 7, 3, ( | 0, 3, 2, 4, 1 ), 16, 28s old, 0 lemmas
% 28.24/28.40 4 : guesser 8, 4, ( 2, 1, 0 | 4, 3 ), 16, 28s old, 3 lemmas
% 28.24/28.40 5 : guesser 16, 11, ( | 2, 4, 1, 3, 5, 0 ), 19, 27s old, 0 lemmas
% 28.24/28.40 6 : guesser 22, 17, ( 2 | 4, 1, 3, 5, 0 ), 30, 27s old, 1 lemmas
% 28.24/28.40 7 : guesser 32, 27, ( 4 | 1, 3, 0, 5, 2 ), 31, 27s old, 2 lemmas
% 28.24/28.40 8 : guesser 67, 62, ( 1 | 3, 0, 2, 5, 4 ), 110, 25s old, 1 lemmas
% 28.24/28.40 9 : guesser 76, 71, ( 1 | 3, 0, 2, 5, 4 ), 121, 24s old, 3 lemmas
% 28.24/28.40 10 : guesser 87, 82, ( | 1, 0 ), 122, 24s old, 0 lemmas
% 28.24/28.40 11 : guesser 106, 101, ( 1, 3 | 0, 2, 5, 4 ), 126, 24s old, 5 lemmas
% 28.24/28.40 12 : guesser 146, 141, ( 0 | 2, 4, 1, 5, 3 ), 151, 23s old, 3 lemmas
% 28.24/28.40 13 : guesser 147, 142, ( | 0, 2, 4, 1, 5, 3 ), 152, 23s old, 0 lemmas
% 28.24/28.40 14 : guesser 156, 151, ( 1 | 3, 0, 2, 5, 4 ), 152, 23s old, 2 lemmas
% 28.24/28.40 15 : guesser 165, 160, ( | 4, 1, 3, 0, 5, 2 ), 153, 23s old, 0 lemmas
% 28.24/28.40 16 : guesser 174, 169, ( | 0, 2, 4, 1, 5, 3 ), 153, 23s old, 0 lemmas
% 28.24/28.40 17 : guesser 175, 170, ( 1 | 3, 0, 2, 5, 4 ), 153, 23s old, 3 lemmas
% 28.24/28.40 18 : guesser 184, 179, ( | 2, 4, 1, 3, 5, 0 ), 154, 23s old, 0 lemmas
% 28.24/28.40 19 : guesser 193, 188, ( | 1, 0 ), 154, 23s old, 0 lemmas
% 28.24/28.40 20 : guesser 195, 190, ( 1 | 3, 0, 2, 5, 4 ), 154, 23s old, 2 lemmas
% 28.24/28.40 21 : guesser 196, 191, ( 4, 1, 3, 0 | 5, 2 ), 155, 23s old, 3 lemmas
% 28.24/28.40 22 : guesser 223, 217, ( | 0, 1 ), 156, 23s old, 0 lemmas
% 28.24/28.40 23 : guesser 224, 218, ( 1 | 0, 5, 4, 3, 6, 2 ), 156, 23s old, 1 lemmas
% 28.24/28.40 24 : guesser 233, 227, ( 4 | 3, 2, 1, 0, 6, 5 ), 157, 23s old, 3 lemmas
% 28.24/28.40 25 : guesser 234, 228, ( | 4, 3, 2, 1, 0, 6, 5 ), 158, 22s old, 0 lemmas
% 28.24/28.40 26 : guesser 244, 238, ( 1 | 0, 5, 4, 3, 6, 2 ), 158, 22s old, 1 lemmas
% 28.24/28.40 27 : guesser 245, 239, ( | 5, 4, 3, 2, 1, 6, 0 ), 159, 22s old, 0 lemmas
% 28.24/28.40 28 : guesser 251, 245, ( 1 | 0, 5, 4, 3, 6, 2 ), 159, 22s old, 3 lemmas
% 28.24/28.40 29 : guesser 252, 246, ( 4 | 3, 2, 1, 0, 6, 5 ), 160, 22s old, 3 lemmas
% 28.24/28.40 30 : guesser 253, 247, ( 1, 0, 5 | 4, 3, 6, 2 ), 162, 22s old, 3 lemmas
% 28.24/28.40 31 : guesser 254, 248, ( | 2, 1, 0, 5, 4, 6, 3 ), 163, 22s old, 0 lemmas
% 28.24/28.40 32 : guesser 263, 257, ( | 0, 5, 4, 3, 2, 6, 1 ), 163, 22s old, 0 lemmas
% 28.24/28.40 33 : guesser 272, 266, ( 2 | 1, 0, 5, 4, 6, 3 ), 163, 22s old, 1 lemmas
% 28.24/28.40 34 : guesser 273, 267, ( | 2, 1, 0, 5, 4, 6, 3 ), 164, 22s old, 0 lemmas
% 28.24/28.40 35 : guesser 282, 276, ( | 4, 3, 2, 1, 0, 6, 5 ), 165, 22s old, 0 lemmas
% 28.24/28.40 36 : guesser 283, 277, ( | 4, 3, 2, 1, 0, 6, 5 ), 165, 22s old, 0 lemmas
% 28.24/28.40 37 : guesser 284, 278, ( | 0, 1 ), 165, 22s old, 0 lemmas
% 28.24/28.40 38 : guesser 288, 282, ( 4, 3, 2, 1 | 0, 6, 5 ), 165, 22s old, 2 lemmas
% 28.24/28.40 39 : guesser 289, 283, ( 0, 5, 4, 3 | 2, 6, 1 ), 167, 22s old, 3 lemmas
% 28.24/28.40 40 : guesser 290, 284, ( | 3, 2, 1, 0, 5, 6, 4 ), 169, 22s old, 0 lemmas
% 28.24/28.40 41 : guesser 291, 285, ( | 3, 2, 1, 0, 5, 6, 4 ), 169, 22s old, 0 lemmas
% 28.24/28.40 42 : guesser 300, 294, ( | 3, 2, 1, 0, 5, 6, 4 ), 169, 22s old, 0 lemmas
% 28.24/28.40 43 : guesser 301, 295, ( 5 | 4, 3, 2, 1, 6, 0 ), 169, 22s old, 2 lemmas
% 28.24/28.40 44 : guesser 302, 296, ( 2, 1, 0, 5, 4 | 6, 3 ), 170, 22s old, 5 lemmas
% 28.24/28.40 45 : guesser 331, 324, ( | 4, 1, 5, 2, 6, 3, 7, 0 ), 197, 21s old, 0 lemmas
% 28.24/28.40 46 : guesser 332, 325, ( 2, 6, 3, 0, 4 | 1, 7, 5 ), 197, 21s old, 1 lemmas
% 28.24/28.40 47 : guesser 333, 326, ( 1 | 5, 2, 6, 3, 0, 7, 4 ), 198, 21s old, 1 lemmas
% 28.24/28.40 48 : guesser 348, 341, ( 5, 2, 6, 3 | 0, 4, 7, 1 ), 398, 1s old, 4 lemmas
% 28.24/28.40 49 : guesser 349, 342, ( 1 | 5, 2, 6, 3, 0, 7, 4 ), 400, 1s old, 1 lemmas
% 28.24/28.40 50 : guesser 357, 350, ( 5, 2, 6, 3 | 0, 4, 7, 1 ), 401, 1s old, 6 lemmas
% 28.24/28.40 51 : guesser 358, 351, ( | 6, 3, 0, 4, 1, 5, 7, 2 ), 403, 1s old, 0 lemmas
% 28.24/28.40 52 : guesser 359, 352, ( 5, 2, 6, 3 | 0, 4, 7, 1 ), 403, 1s old, 6 lemmas
% 28.24/28.40 53 : guesser 360, 353, ( | 2, 6, 3, 0, 4, 1, 7, 5 ), 405, 1s old, 0 lemmas
% 28.24/28.40 54 : guesser 361, 354, ( | 5, 2, 6, 3, 0, 4, 7, 1 ), 405, 1s old, 0 lemmas
% 28.24/28.40 55 : guesser 362, 355, ( 3 | 0, 4, 1, 5, 2, 7, 6 ), 405, 1s old, 1 lemmas
% 28.24/28.40 56 : guesser 363, 356, ( | 4, 1, 5, 2, 6, 3, 7, 0 ), 406, 1s old, 0 lemmas
% 28.24/28.40 57 : guesser 372, 365, ( 2, 6, 3, 0, 4 | 1, 7, 5 ), 406, 1s old, 3 lemmas
% 28.24/28.40 58 : guesser 373, 366, ( | 0, 4, 1, 5, 2, 6, 7, 3 ), 407, 1s old, 0 lemmas
% 28.24/28.40 59 : guesser 374, 367, ( 5, 2, 6, 3, 0, 4 | 7, 1 ), 407, 1s old, 6 lemmas
% 28.24/28.40 60 : guesser 380, 372, ( 0, 7 | 6, 5, 4, 3, 2, 8, 1 ), 409, 0s old, 4 lemmas
% 28.24/28.40 61 : guesser 381, 373, ( | 3, 2, 1, 0, 7, 6, 5, 8, 4 ), 411, 0s old, 0 lemmas
% 28.24/28.40 62 : guesser 382, 374, ( 6 | 5, 4, 3, 2, 1, 0, 8, 7 ), 411, 0s old, 3 lemmas
% 28.24/28.40 63 : guesser 383, 375, ( | 1, 0, 7, 6, 5, 4, 3, 8, 2 ), 412, 0s old, 0 lemmas
% 28.24/28.40 64 : guesser 384, 376, ( | 0, 1 ), 412, 0s old, 0 lemmas
% 28.24/28.40 65 : guesser 385, 377, ( 0, 7 | 6, 5, 4, 3, 2, 8, 1 ), 412, 0s old, 1 lemmas
% 28.24/28.40 66 : guesser 386, 378, ( | 7, 6, 5, 4, 3, 2, 1, 8, 0 ), 413, 0s old, 0 lemmas
% 28.24/28.40 67 : guesser 387, 379, ( | 5, 4, 3, 2, 1, 0, 7, 8, 6 ), 413, 0s old, 0 lemmas
% 28.24/28.40 68 : guesser 389, 381, ( 0 | 7, 6, 5, 4, 3, 2, 8, 1 ), 413, 0s old, 1 lemmas
% 28.24/28.40 69 : guesser 390, 382, ( 0, 7 | 6, 5, 4, 3, 2, 8, 1 ), 414, 0s old, 1 lemmas
% 28.24/28.40 70 : guesser 391, 383, ( 6, 5 | 4, 3, 2, 1, 0, 8, 7 ), 415, 0s old, 2 lemmas
% 28.24/28.40 71 : guesser 392, 384, ( | 6, 5, 4, 3, 2, 1, 0, 8, 7 ), 416, 0s old, 0 lemmas
% 28.24/28.40 72 : guesser 393, 385, ( | 0, 7, 6, 5, 4, 3, 2, 8, 1 ), 416, 0s old, 0 lemmas
% 28.24/28.40 73 : guesser 395, 387, ( 1 | 0, 7, 6, 5, 4, 3, 8, 2 ), 416, 0s old, 2 lemmas
% 28.24/28.40 74 : guesser 396, 388, ( 1 | 0, 7, 6, 5, 4, 3, 8, 2 ), 417, 0s old, 2 lemmas
% 28.24/28.40 75 : guesser 397, 389, ( 6 | 5, 4, 3, 2, 1, 0, 8, 7 ), 418, 0s old, 3 lemmas
% 28.24/28.40 76 : guesser 398, 390, ( | 7, 6, 5, 4, 3, 2, 1, 8, 0 ), 419, 0s old, 0 lemmas
% 28.24/28.40 77 : guesser 422, 414, ( | 1, 0 ), 419, 0s old, 0 lemmas
% 28.24/28.40 78 : guesser 423, 415, ( | 2, 1, 0, 7, 6, 5, 4, 8, 3 ), 419, 0s old, 0 lemmas
% 28.24/28.40 79 : guesser 426, 418, ( 0 | 7, 6, 5, 4, 3, 2, 8, 1 ), 419, 0s old, 3 lemmas
% 28.24/28.40 80 : guesser 427, 419, ( 3, 2, 1 | 0, 7, 6, 5, 8, 4 ), 421, 0s old, 3 lemmas
% 28.24/28.40 81 : guesser 428, 420, ( 0 | 7, 6, 5, 4, 3, 2, 8, 1 ), 423, 0s old, 1 lemmas
% 28.24/28.40 82 : guesser 429, 421, ( 2 | 1, 0, 7, 6, 5, 4, 8, 3 ), 424, 0s old, 3 lemmas
% 28.24/28.40
% 28.24/28.40 Elements:
% 28.24/28.40 { E0, E1, E2, E3, E4, E5, E6, E7 }
% 28.24/28.40
% 28.24/28.40 Atoms:
% 28.24/28.40 0 : #-{T} E0 { }
% 28.24/28.40 1 : #-{T} E1 { 0 }
% 28.24/28.40 2 : P_tptp0-{T}(E1) { 0 }
% 28.24/28.40 3 : #-{T} E2 { 1 }
% 28.24/28.40 4 : P_tptp3-{T}(E2) { 1 }
% 28.24/28.40 5 : #-{T} E3 { 2 }
% 28.24/28.40 6 : P_tptp4-{T}(E3) { 2 }
% 28.24/28.40 7 : P_tptp1-{T}(E0) { 3 }
% 28.24/28.40 8 : #-{T} E4 { 4 }
% 28.24/28.40 9 : P_tptp2-{T}(E4) { 4 }
% 28.24/28.40 10 : activity-{T}(E1) { 0, 1, 2, 3, 4 }
% 28.24/28.40 11 : atomic-{T}(E3) { 0, 1, 2, 3, 4 }
% 28.24/28.40 12 : atomic-{T}(E0) { 0, 1, 2, 3, 4 }
% 28.24/28.40 13 : subactivity-{T}(E1,E1) { 0, 1, 2, 3, 4 }
% 28.24/28.40 14 : atomic-{T}(E4) { 0, 1, 2, 3, 4 }
% 28.24/28.40 15 : atomic-{T}(E2) { 0, 1, 2, 3, 4 }
% 28.24/28.40 16 : pppp28-{T}(E2,E1,E0,E4,E2) { 0, 1, 2, 3, 4, 5 }
% 28.24/28.40 17 : occurrence_of-{T}(E2,E1) { 0, 1, 2, 3, 4, 5 }
% 28.24/28.40 18 : activity_occurrence-{T}(E2) { 0, 1, 2, 3, 4, 5 }
% 28.24/28.40 19 : pppp6-{T}(E2,E1) { 0, 1, 2, 3, 4, 5 }
% 28.24/28.40 20 : pppp34-{T}(E2,E1) { 0, 1, 2, 3, 4, 5 }
% 28.24/28.40 21 : subactivity_occurrence-{T}(E2,E2) { 0, 1, 2, 3, 4, 5 }
% 28.24/28.40 22 : pppp17-{T}(E2,E1,E4) { 0, 1, 2, 3, 4, 5, 6 }
% 28.24/28.40 23 : subactivity_occurrence-{T}(E4,E2) { 0, 1, 2, 3, 4, 5, 6 }
% 28.24/28.40 24 : root-{T}(E4,E1) { 0, 1, 2, 3, 4, 5, 6 }
% 28.24/28.40 25 : legal-{T}(E4) { 0, 1, 2, 3, 4, 5, 6 }
% 28.24/28.40 26 : activity_occurrence-{T}(E4) { 0, 1, 2, 3, 4, 5, 6 }
% 28.24/28.40 27 : pppp4-{T}(E4,E2) { 0, 1, 2, 3, 4, 5, 6 }
% 28.24/28.40 28 : arboreal-{T}(E4) { 0, 1, 2, 3, 4, 5, 6 }
% 28.24/28.40 29 : root_occ-{T}(E4,E2) { 0, 1, 2, 3, 4, 5, 6 }
% 28.24/28.40 30 : pppp19-{T}(E4,E2,E1) { 0, 1, 2, 3, 4, 5, 6 }
% 28.24/28.40 31 : pppp33-{T}(E4,E1) { 0, 1, 2, 3, 4, 5, 6 }
% 28.24/28.40 32 : pppp24-{T}(E2,E1,E1,E0,E4,E3,E2) { 0, 1, 2, 3, 4, 5, 7 }
% 28.24/28.40 33 : leaf_occ-{T}(E1,E2) { 0, 1, 2, 3, 4, 5, 7 }
% 28.24/28.40 34 : pppp5-{T}(E1,E2) { 0, 1, 2, 3, 4, 5, 7 }
% 28.24/28.40 35 : min_precedes-{T}(E4,E1,E1) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 36 : subactivity_occurrence-{T}(E1,E2) { 0, 1, 2, 3, 4, 5, 7 }
% 28.24/28.40 37 : pppp20-{T}(E1,E2,E1) { 0, 1, 2, 3, 4, 5, 7 }
% 28.24/28.40 38 : precedes-{T}(E4,E1) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 39 : activity_occurrence-{T}(E1) { 0, 1, 2, 3, 4, 5, 7 }
% 28.24/28.40 40 : leaf-{T}(E1,E1) { 0, 1, 2, 3, 4, 5, 7 }
% 28.24/28.40 41 : pppp0-{T}(E4,E1) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 42 : pppp1-{T}(E1,E1) { 0, 1, 2, 3, 4, 5, 7 }
% 28.24/28.40 43 : pppp36-{T}(E1,E1) { 0, 1, 2, 3, 4, 5, 7 }
% 28.24/28.40 44 : earlier-{T}(E4,E1) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 45 : legal-{T}(E1) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 46 : pppp30-{T}(E4,E1) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 47 : arboreal-{T}(E1) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 48 : pppp29-{T}(E1,E1) { 0, 1, 2, 3, 4, 5, 7 }
% 28.24/28.40 49 : pppp10-{T}(E1,E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 50 : pppp6-{T}(E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 51 : occurrence_of-{T}(E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 52 : activity-{T}(E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 53 : subactivity-{T}(E2,E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 54 : pppp3-{T}(E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 55 : subactivity_occurrence-{T}(E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 56 : atocc-{T}(E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 57 : pppp14-{T}(E4,E2,E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 58 : root-{T}(E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 59 : pppp4-{T}(E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 60 : root_occ-{T}(E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 61 : pppp19-{T}(E4,E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 62 : pppp1-{T}(E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 63 : leaf-{T}(E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 64 : pppp5-{T}(E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 65 : leaf_occ-{T}(E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 66 : pppp20-{T}(E4,E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7 }
% 28.24/28.40 67 : pppp9-{T}(E4,E1,E3) { 0, 1, 2, 3, 4, 5, 6, 8 }
% 28.24/28.40 68 : atocc-{T}(E4,E3) { 0, 1, 2, 3, 4, 5, 6, 8 }
% 28.24/28.40 69 : subactivity-{T}(E3,E1) { 0, 1, 2, 3, 4, 5, 6, 8 }
% 28.24/28.40 70 : pppp3-{T}(E4,E3) { 0, 1, 2, 3, 4, 5, 6, 8 }
% 28.24/28.40 71 : root-{T}(E4,E3) { 0, 1, 2, 3, 4, 5, 6, 8 }
% 28.24/28.40 72 : pppp1-{T}(E4,E3) { 0, 1, 2, 3, 4, 5, 6, 8 }
% 28.24/28.40 73 : pppp14-{T}(E4,E3,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 8 }
% 28.24/28.40 74 : leaf-{T}(E4,E3) { 0, 1, 2, 3, 4, 5, 6, 8 }
% 28.24/28.40 75 : subactivity-{T}(E3,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 8 }
% 28.24/28.40 76 : pppp16-{T}(E4,E1,E3) { 0, 1, 2, 3, 4, 5, 6, 9 }
% 28.24/28.40 77 : subactivity_occurrence-{T}(E4,E3) { 0, 1, 2, 3, 4, 5, 6, 9 }
% 28.24/28.40 78 : occurrence_of-{T}(E3,E1) { 0, 1, 2, 3, 4, 5, 6, 9 }
% 28.24/28.40 79 : activity_occurrence-{T}(E3) { 0, 1, 2, 3, 4, 5, 6, 9 }
% 28.24/28.40 80 : pppp4-{T}(E4,E3) { 0, 1, 2, 3, 4, 5, 6, 9 }
% 28.24/28.40 81 : root_occ-{T}(E4,E3) { 0, 1, 2, 3, 4, 5, 6, 9 }
% 28.24/28.40 82 : pppp6-{T}(E3,E1) { 0, 1, 2, 3, 4, 5, 6, 9 }
% 28.24/28.40 83 : pppp19-{T}(E4,E3,E1) { 0, 1, 2, 3, 4, 5, 6, 9 }
% 28.24/28.40 84 : subactivity_occurrence-{T}(E3,E3) { 0, 1, 2, 3, 4, 5, 6, 9 }
% 28.24/28.40 85 : pppp34-{T}(E3,E1) { 0, 1, 2, 3, 4, 5, 6, 9 }
% 28.24/28.40 86 : pppp17-{T}(E3,E1,E4) { 0, 1, 2, 3, 4, 5, 6, 9 }
% 28.24/28.40 87 : occurrence_of-{T}(E1,E4) { 0, 1, 2, 3, 4, 5, 7, 10 }
% 28.24/28.40 88 : activity-{T}(E4) { 0, 1, 2, 3, 4, 5, 7, 10 }
% 28.24/28.40 89 : pppp27-{T}(E2,E1,E1,E0,E4,E2) { 0, 1, 2, 3, 4, 5, 7, 10 }
% 28.24/28.40 90 : subactivity-{T}(E4,E4) { 0, 1, 2, 3, 4, 5, 7, 10 }
% 28.24/28.40 91 : pppp6-{T}(E1,E4) { 0, 1, 2, 3, 4, 5, 7, 10 }
% 28.24/28.40 92 : pppp3-{T}(E1,E4) { 0, 1, 2, 3, 4, 5, 7, 10 }
% 28.24/28.40 93 : subactivity_occurrence-{T}(E1,E1) { 0, 1, 2, 3, 4, 5, 7, 10 }
% 28.24/28.40 94 : atocc-{T}(E1,E4) { 0, 1, 2, 3, 4, 5, 7, 10 }
% 28.24/28.40 95 : pppp14-{T}(E1,E4,E4) { 0, 1, 2, 3, 4, 5, 7, 10 }
% 28.24/28.40 96 : root-{T}(E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10 }
% 28.24/28.40 97 : pppp1-{T}(E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10 }
% 28.24/28.40 98 : pppp4-{T}(E1,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10 }
% 28.24/28.40 99 : leaf-{T}(E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10 }
% 28.24/28.40 100 : root_occ-{T}(E1,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10 }
% 28.24/28.40 101 : pppp19-{T}(E1,E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10 }
% 28.24/28.40 102 : pppp5-{T}(E1,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10 }
% 28.24/28.40 103 : leaf_occ-{T}(E1,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10 }
% 28.24/28.40 104 : pppp20-{T}(E1,E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10 }
% 28.24/28.40 105 : pppp40-{T}(E4,E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10 }
% 28.24/28.40 106 : pppp11-{T}(E1,E1,E0) { 0, 1, 2, 3, 4, 5, 7, 11 }
% 28.24/28.40 107 : min_precedes-{T}(E0,E1,E1) { 0, 1, 2, 3, 4, 5, 7, 11 }
% 28.24/28.40 108 : precedes-{T}(E0,E1) { 0, 1, 2, 3, 4, 5, 7, 11 }
% 28.24/28.40 109 : arboreal-{T}(E0) { 0, 1, 2, 3, 4, 5, 7, 11 }
% 28.24/28.40 110 : subactivity_occurrence-{T}(E0,E2) { 0, 1, 2, 3, 4, 5, 7, 11 }
% 28.24/28.40 111 : pppp0-{T}(E0,E1) { 0, 1, 2, 3, 4, 5, 7, 11 }
% 28.24/28.40 112 : activity_occurrence-{T}(E0) { 0, 1, 2, 3, 4, 5, 7, 11 }
% 28.24/28.40 113 : min_precedes-{T}(E4,E0,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 114 : earlier-{T}(E0,E1) { 0, 1, 2, 3, 4, 5, 7, 11 }
% 28.24/28.40 115 : precedes-{T}(E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 116 : pppp31-{T}(E0,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 117 : pppp0-{T}(E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 118 : legal-{T}(E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 119 : pppp32-{T}(E4,E1,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 120 : earlier-{T}(E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 121 : pppp10-{T}(E0,E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 122 : pppp23-{T}(E2,E0,E1,E1,E3,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 123 : next_subocc-{T}(E0,E1,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 124 : occurrence_of-{T}(E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 125 : pppp22-{T}(E2,E4,E0,E1,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 126 : activity-{T}(E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 127 : pppp2-{T}(E0,E1,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 128 : next_subocc-{T}(E4,E0,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 129 : subactivity-{T}(E3,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 130 : pppp2-{T}(E4,E0,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 131 : pppp6-{T}(E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 132 : pppp3-{T}(E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 133 : subactivity_occurrence-{T}(E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 134 : pppp35-{T}(E0,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 8, 11 }
% 28.24/28.40 135 : atocc-{T}(E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 136 : pppp14-{T}(E0,E3,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 137 : root-{T}(E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 138 : pppp1-{T}(E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 139 : pppp4-{T}(E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 140 : leaf-{T}(E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 141 : root_occ-{T}(E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 142 : pppp19-{T}(E0,E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 143 : pppp5-{T}(E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 144 : leaf_occ-{T}(E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 145 : pppp20-{T}(E0,E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11 }
% 28.24/28.40 146 : pppp21-{T}(E1,E1,E2) { 0, 1, 2, 3, 4, 5, 7, 12 }
% 28.24/28.40 147 : pppp7-{T}(E4,E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 13 }
% 28.24/28.40 148 : atocc-{T}(E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 13 }
% 28.24/28.40 149 : subactivity-{T}(E0,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 13 }
% 28.24/28.40 150 : pppp3-{T}(E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 13 }
% 28.24/28.40 151 : root-{T}(E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 13 }
% 28.24/28.40 152 : pppp14-{T}(E4,E0,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 13 }
% 28.24/28.40 153 : pppp1-{T}(E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 13 }
% 28.24/28.40 154 : leaf-{T}(E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 13 }
% 28.24/28.40 155 : subactivity-{T}(E0,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 13 }
% 28.24/28.40 156 : pppp8-{T}(E1,E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 14 }
% 28.24/28.40 157 : atocc-{T}(E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 14 }
% 28.24/28.40 158 : pppp3-{T}(E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 14 }
% 28.24/28.40 159 : root-{T}(E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 14 }
% 28.24/28.40 160 : pppp1-{T}(E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 14 }
% 28.24/28.40 161 : pppp14-{T}(E1,E3,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14 }
% 28.24/28.40 162 : leaf-{T}(E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 14 }
% 28.24/28.40 163 : subactivity-{T}(E3,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14 }
% 28.24/28.40 164 : pppp35-{T}(E0,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 14 }
% 28.24/28.40 165 : pppp9-{T}(E4,E2,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 15 }
% 28.24/28.40 166 : atocc-{T}(E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 15 }
% 28.24/28.40 167 : subactivity-{T}(E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 15 }
% 28.24/28.40 168 : pppp3-{T}(E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 15 }
% 28.24/28.40 169 : root-{T}(E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 15 }
% 28.24/28.40 170 : pppp14-{T}(E4,E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 15 }
% 28.24/28.40 171 : pppp1-{T}(E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 15 }
% 28.24/28.40 172 : pppp35-{T}(E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15 }
% 28.24/28.40 173 : leaf-{T}(E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 15 }
% 28.24/28.40 174 : pppp12-{T}(E4,E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 16 }
% 28.24/28.40 175 : pppp15-{T}(E4,E1,E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 17 }
% 28.24/28.40 176 : subactivity_occurrence-{T}(E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 17 }
% 28.24/28.40 177 : pppp5-{T}(E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 17 }
% 28.24/28.40 178 : subactivity_occurrence-{T}(E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 11, 17 }
% 28.24/28.40 179 : leaf_occ-{T}(E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 17 }
% 28.24/28.40 180 : pppp20-{T}(E1,E3,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 17 }
% 28.24/28.40 181 : pppp24-{T}(E3,E1,E1,E0,E4,E3,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 17 }
% 28.24/28.40 182 : pppp23-{T}(E3,E0,E1,E1,E3,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 11, 17 }
% 28.24/28.40 183 : pppp22-{T}(E3,E4,E0,E1,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 11, 17 }
% 28.24/28.40 184 : pppp9-{T}(E4,E3,E2) { 0, 1, 2, 3, 4, 5, 6, 8, 18 }
% 28.24/28.40 185 : subactivity-{T}(E2,E3) { 0, 1, 2, 3, 4, 5, 6, 8, 18 }
% 28.24/28.40 186 : pppp3-{T}(E0,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 8, 11, 18 }
% 28.24/28.40 187 : pppp35-{T}(E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 8, 11, 18 }
% 28.24/28.40 188 : atocc-{T}(E0,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 8, 11, 18 }
% 28.24/28.40 189 : pppp14-{T}(E0,E2,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 8, 11, 18 }
% 28.24/28.40 190 : root-{T}(E0,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 8, 11, 18 }
% 28.24/28.40 191 : pppp1-{T}(E0,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 8, 11, 18 }
% 28.24/28.40 192 : leaf-{T}(E0,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 8, 11, 18 }
% 28.24/28.40 193 : pppp35-{T}(E3,E2) { 0, 1, 2, 3, 4, 5, 6, 9, 19 }
% 28.24/28.40 194 : pppp35-{T}(E2,E3) { 0, 1, 2, 3, 4, 5, 6, 9, 19 }
% 28.24/28.40 195 : pppp9-{T}(E1,E4,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 20 }
% 28.24/28.40 196 : #-{T} E5 { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 197 : pppp26-{T}(E4,E5,E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 198 : min_precedes-{T}(E4,E5,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 199 : occurrence_of-{T}(E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 200 : activity-{T}(E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 201 : activity_occurrence-{T}(E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 202 : precedes-{T}(E4,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 203 : subactivity-{T}(E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 204 : pppp0-{T}(E4,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 205 : arboreal-{T}(E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 206 : earlier-{T}(E4,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 207 : legal-{T}(E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 208 : pppp6-{T}(E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 209 : pppp3-{T}(E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 210 : subactivity_occurrence-{T}(E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 211 : pppp35-{T}(E5,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 13, 21 }
% 28.24/28.40 212 : atocc-{T}(E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 213 : pppp14-{T}(E5,E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 214 : root-{T}(E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 215 : pppp1-{T}(E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 216 : pppp4-{T}(E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 217 : leaf-{T}(E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 218 : root_occ-{T}(E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 219 : pppp19-{T}(E5,E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 220 : pppp5-{T}(E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 221 : leaf_occ-{T}(E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 222 : pppp20-{T}(E5,E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21 }
% 28.24/28.40 223 : pppp37-{T}(E4,E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 22 }
% 28.24/28.40 224 : pppp7-{T}(E0,E1,E0) { 0, 1, 2, 3, 4, 5, 7, 11, 23 }
% 28.24/28.40 225 : atocc-{T}(E0,E0) { 0, 1, 2, 3, 4, 5, 7, 11, 23 }
% 28.24/28.40 226 : pppp3-{T}(E0,E0) { 0, 1, 2, 3, 4, 5, 7, 11, 23 }
% 28.24/28.40 227 : root-{T}(E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23 }
% 28.24/28.40 228 : pppp14-{T}(E0,E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23 }
% 28.24/28.40 229 : pppp1-{T}(E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23 }
% 28.24/28.40 230 : leaf-{T}(E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23 }
% 28.24/28.40 231 : subactivity-{T}(E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23 }
% 28.24/28.40 232 : pppp35-{T}(E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 23 }
% 28.24/28.40 233 : pppp15-{T}(E0,E1,E1,E3) { 0, 1, 2, 3, 4, 5, 7, 11, 24 }
% 28.24/28.40 234 : pppp8-{T}(E0,E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 25 }
% 28.24/28.40 235 : atocc-{T}(E0,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 25 }
% 28.24/28.40 236 : subactivity-{T}(E4,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 25 }
% 28.24/28.40 237 : pppp3-{T}(E0,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 25 }
% 28.24/28.40 238 : root-{T}(E0,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 25 }
% 28.24/28.40 239 : pppp14-{T}(E0,E4,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 25 }
% 28.24/28.40 240 : pppp1-{T}(E0,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 25 }
% 28.24/28.40 241 : leaf-{T}(E0,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 25 }
% 28.24/28.40 242 : subactivity-{T}(E4,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 25 }
% 28.24/28.40 243 : pppp35-{T}(E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 25 }
% 28.24/28.40 244 : pppp9-{T}(E0,E3,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 26 }
% 28.24/28.40 245 : pppp12-{T}(E0,E1,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 27 }
% 28.24/28.40 246 : min_precedes-{T}(E0,E5,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 27 }
% 28.24/28.40 247 : precedes-{T}(E0,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 27 }
% 28.24/28.40 248 : pppp32-{T}(E4,E5,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 27 }
% 28.24/28.40 249 : pppp0-{T}(E0,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 27 }
% 28.24/28.40 250 : earlier-{T}(E0,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 27 }
% 28.24/28.40 251 : pppp13-{T}(E4,E1,E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 28 }
% 28.24/28.40 252 : pppp15-{T}(E4,E0,E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 29 }
% 28.24/28.40 253 : pppp18-{T}(E0,E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 8, 11, 30 }
% 28.24/28.40 254 : pppp9-{T}(E4,E0,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 13, 31 }
% 28.24/28.40 255 : subactivity-{T}(E2,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 13, 31 }
% 28.24/28.40 256 : pppp3-{T}(E5,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 13, 21, 31 }
% 28.24/28.40 257 : pppp35-{T}(E4,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 13, 21, 31 }
% 28.24/28.40 258 : atocc-{T}(E5,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 13, 21, 31 }
% 28.24/28.40 259 : pppp14-{T}(E5,E2,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 13, 21, 31 }
% 28.24/28.40 260 : root-{T}(E5,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 13, 21, 31 }
% 28.24/28.40 261 : pppp1-{T}(E5,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 13, 21, 31 }
% 28.24/28.40 262 : leaf-{T}(E5,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 13, 21, 31 }
% 28.24/28.40 263 : pppp9-{T}(E1,E3,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 14, 32 }
% 28.24/28.40 264 : atocc-{T}(E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 14, 32 }
% 28.24/28.40 265 : pppp3-{T}(E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 14, 32 }
% 28.24/28.40 266 : root-{T}(E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 14, 32 }
% 28.24/28.40 267 : pppp1-{T}(E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 14, 32 }
% 28.24/28.40 268 : pppp14-{T}(E1,E0,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 32 }
% 28.24/28.40 269 : leaf-{T}(E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 14, 32 }
% 28.24/28.40 270 : subactivity-{T}(E0,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 32 }
% 28.24/28.40 271 : pppp35-{T}(E5,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 21, 32 }
% 28.24/28.40 272 : pppp18-{T}(E0,E1,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 14, 33 }
% 28.24/28.40 273 : pppp9-{T}(E4,E4,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 15, 34 }
% 28.24/28.40 274 : subactivity-{T}(E2,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 15, 34 }
% 28.24/28.40 275 : pppp3-{T}(E1,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34 }
% 28.24/28.40 276 : pppp35-{T}(E4,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34 }
% 28.24/28.40 277 : atocc-{T}(E1,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34 }
% 28.24/28.40 278 : pppp14-{T}(E1,E2,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34 }
% 28.24/28.40 279 : root-{T}(E1,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34 }
% 28.24/28.40 280 : pppp1-{T}(E1,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34 }
% 28.24/28.40 281 : leaf-{T}(E1,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34 }
% 28.24/28.40 282 : pppp18-{T}(E1,E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 35 }
% 28.24/28.40 283 : pppp9-{T}(E0,E2,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 8, 11, 18, 36 }
% 28.24/28.40 284 : pppp1-{T}(E5,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 37 }
% 28.24/28.40 285 : leaf-{T}(E5,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 37 }
% 28.24/28.40 286 : pppp29-{T}(E5,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 37 }
% 28.24/28.40 287 : pppp36-{T}(E5,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 37 }
% 28.24/28.40 288 : pppp18-{T}(E4,E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 8, 11, 18, 38 }
% 28.24/28.40 289 : pppp18-{T}(E3,E2,E2) { 0, 1, 2, 3, 4, 5, 6, 9, 19, 39 }
% 28.24/28.40 290 : pppp18-{T}(E2,E3,E3) { 0, 1, 2, 3, 4, 5, 6, 9, 19, 40 }
% 28.24/28.40 291 : pppp8-{T}(E5,E1,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 41 }
% 28.24/28.40 292 : atocc-{T}(E5,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 41 }
% 28.24/28.40 293 : pppp3-{T}(E5,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 41 }
% 28.24/28.40 294 : root-{T}(E5,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 41 }
% 28.24/28.40 295 : pppp14-{T}(E5,E3,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 41 }
% 28.24/28.40 296 : pppp1-{T}(E5,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 41 }
% 28.24/28.40 297 : leaf-{T}(E5,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 41 }
% 28.24/28.40 298 : subactivity-{T}(E3,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 41 }
% 28.24/28.40 299 : pppp35-{T}(E0,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 41 }
% 28.24/28.40 300 : pppp9-{T}(E5,E0,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 42 }
% 28.24/28.40 301 : pppp10-{T}(E5,E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 43 }
% 28.24/28.40 302 : #-{T} E6 { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 303 : pppp15-{T}(E4,E5,E1,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 304 : subactivity_occurrence-{T}(E5,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 305 : subactivity_occurrence-{T}(E4,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 306 : occurrence_of-{T}(E6,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 307 : activity_occurrence-{T}(E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 308 : pppp4-{T}(E4,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 309 : root_occ-{T}(E4,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 310 : pppp6-{T}(E6,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 311 : pppp19-{T}(E4,E6,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 312 : subactivity_occurrence-{T}(E6,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 313 : pppp34-{T}(E6,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 314 : subactivity_occurrence-{T}(E0,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 27, 44 }
% 28.24/28.40 315 : pppp17-{T}(E6,E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 44 }
% 28.24/28.40 316 : pppp5-{T}(E5,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 37, 44 }
% 28.24/28.40 317 : leaf_occ-{T}(E5,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 37, 44 }
% 28.24/28.40 318 : pppp20-{T}(E5,E6,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 37, 44 }
% 28.24/28.40 319 : pppp24-{T}(E6,E5,E1,E0,E4,E3,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 37, 44 }
% 28.24/28.40 320 : pppp23-{T}(E6,E0,E5,E1,E3,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 27, 37, 44 }
% 28.24/28.40 321 : next_subocc-{T}(E0,E5,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 27, 37, 44 }
% 28.24/28.40 322 : pppp22-{T}(E6,E4,E0,E1,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 27, 37, 44 }
% 28.24/28.40 323 : pppp2-{T}(E0,E5,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 27, 37, 44 }
% 28.24/28.40 324 : pppp35-{T}(E5,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 13, 21, 27, 37, 44 }
% 28.24/28.40 325 : pppp35-{T}(E5,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 10, 11, 13, 17, 21, 27, 37, 44 }
% 28.24/28.40 326 : pppp35-{T}(E1,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 25, 27, 37, 44 }
% 28.24/28.41 327 : pppp35-{T}(E6,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 10, 11, 17, 21, 27, 37, 44 }
% 28.24/28.41 328 : pppp35-{T}(E6,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 27, 37, 44 }
% 28.24/28.41 329 : pppp35-{T}(E3,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 10, 11, 17, 21, 27, 37, 44 }
% 28.24/28.41 330 : pppp35-{T}(E2,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 27, 37, 44 }
% 28.24/28.41 331 : pppp18-{T}(E5,E4,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 13, 21, 45 }
% 28.24/28.41 332 : pppp25-{T}(E4,E1,E1,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 22, 46 }
% 28.24/28.41 333 : pppp9-{T}(E0,E0,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47 }
% 28.24/28.41 334 : atocc-{T}(E0,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47 }
% 28.24/28.41 335 : subactivity-{T}(E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47 }
% 28.24/28.41 336 : pppp3-{T}(E0,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47 }
% 28.24/28.41 337 : root-{T}(E0,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47 }
% 28.24/28.41 338 : pppp3-{T}(E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 23, 47 }
% 28.24/28.41 339 : pppp14-{T}(E0,E5,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47 }
% 28.24/28.41 340 : atocc-{T}(E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 23, 47 }
% 28.24/28.41 341 : subactivity-{T}(E5,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47 }
% 28.24/28.41 342 : root-{T}(E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 23, 47 }
% 28.24/28.41 343 : pppp14-{T}(E5,E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 23, 47 }
% 28.24/28.41 344 : pppp1-{T}(E0,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47 }
% 28.24/28.41 345 : leaf-{T}(E0,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47 }
% 28.24/28.41 346 : pppp1-{T}(E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 23, 47 }
% 28.24/28.41 347 : leaf-{T}(E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 23, 47 }
% 28.24/28.41 348 : pppp18-{T}(E5,E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 23, 48 }
% 28.24/28.41 349 : pppp9-{T}(E0,E4,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 25, 49 }
% 28.24/28.41 350 : subactivity-{T}(E5,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 25, 49 }
% 28.24/28.41 351 : pppp3-{T}(E1,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 25, 49 }
% 28.24/28.41 352 : atocc-{T}(E1,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 25, 49 }
% 28.24/28.41 353 : pppp14-{T}(E1,E5,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 25, 49 }
% 28.24/28.41 354 : root-{T}(E1,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 25, 49 }
% 28.24/28.41 355 : pppp1-{T}(E1,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 25, 49 }
% 28.24/28.41 356 : leaf-{T}(E1,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 25, 49 }
% 28.24/28.41 357 : pppp18-{T}(E1,E0,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 25, 50 }
% 28.24/28.41 358 : pppp15-{T}(E0,E5,E1,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 27, 51 }
% 28.24/28.41 359 : pppp13-{T}(E4,E5,E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 27, 52 }
% 28.24/28.41 360 : pppp9-{T}(E5,E2,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 13, 21, 31, 53 }
% 28.24/28.41 361 : pppp18-{T}(E4,E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 13, 21, 31, 54 }
% 28.24/28.41 362 : pppp11-{T}(E5,E1,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 37, 55 }
% 28.24/28.41 363 : pppp9-{T}(E1,E0,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 14, 32, 56 }
% 28.24/28.41 364 : subactivity-{T}(E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 14, 32, 56 }
% 28.24/28.41 365 : pppp3-{T}(E5,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 21, 32, 56 }
% 28.24/28.41 366 : pppp35-{T}(E1,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 21, 32, 56 }
% 28.24/28.41 367 : atocc-{T}(E5,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 21, 32, 56 }
% 28.24/28.41 368 : pppp14-{T}(E5,E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 21, 32, 56 }
% 28.24/28.41 369 : root-{T}(E5,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 21, 32, 56 }
% 28.24/28.41 370 : pppp1-{T}(E5,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 21, 32, 56 }
% 28.24/28.41 371 : leaf-{T}(E5,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 21, 32, 56 }
% 28.24/28.41 372 : pppp18-{T}(E5,E1,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 21, 32, 57 }
% 28.24/28.41 373 : pppp9-{T}(E1,E2,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 58 }
% 28.24/28.41 374 : #-{T} E7 { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59 }
% 28.24/28.41 375 : pppp18-{T}(E4,E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59 }
% 28.24/28.41 376 : subactivity_occurrence-{T}(E7,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59 }
% 28.24/28.41 377 : activity_occurrence-{T}(E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59 }
% 28.24/28.41 378 : subactivity_occurrence-{T}(E7,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59 }
% 28.24/28.41 379 : subactivity_occurrence-{T}(E7,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 17, 34, 59 }
% 28.24/28.41 380 : pppp21-{T}(E5,E1,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 37, 60 }
% 28.24/28.41 381 : pppp9-{T}(E5,E3,E3) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 21, 41, 61 }
% 28.24/28.41 382 : pppp18-{T}(E0,E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 41, 62 }
% 28.24/28.41 383 : pppp18-{T}(E6,E2,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 27, 37, 44, 63 }
% 28.24/28.41 384 : atomic-{T}(E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47, 64 }
% 28.24/28.41 385 : pppp18-{T}(E2,E6,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 27, 37, 44, 65 }
% 28.24/28.41 386 : pppp18-{T}(E5,E2,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 13, 21, 27, 37, 44, 66 }
% 28.24/28.41 387 : pppp9-{T}(E0,E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47, 67 }
% 28.24/28.41 388 : subactivity-{T}(E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 11, 23, 47, 67 }
% 28.24/28.41 389 : pppp18-{T}(E6,E3,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 10, 11, 17, 21, 27, 37, 44, 68 }
% 28.24/28.41 390 : pppp18-{T}(E3,E6,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 10, 11, 17, 21, 27, 37, 44, 69 }
% 28.24/28.41 391 : pppp18-{T}(E5,E3,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 9, 10, 11, 13, 17, 21, 27, 37, 44, 70 }
% 28.24/28.41 392 : pppp18-{T}(E1,E6,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 25, 27, 37, 44, 71 }
% 28.24/28.41 393 : pppp9-{T}(E5,E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 23, 47, 72 }
% 28.24/28.41 394 : subactivity-{T}(E0,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 21, 23, 47, 72 }
% 28.24/28.41 395 : pppp9-{T}(E1,E5,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 25, 49, 73 }
% 28.24/28.41 396 : pppp9-{T}(E5,E4,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 21, 32, 56, 74 }
% 28.24/28.41 397 : pppp18-{T}(E1,E5,E5) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 14, 21, 32, 56, 75 }
% 28.24/28.41 398 : pppp6-{T}(E7,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 399 : occurrence_of-{T}(E7,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 400 : activity-{T}(E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 401 : subactivity-{T}(E7,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 402 : pppp34-{T}(E7,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 403 : subactivity_occurrence-{T}(E7,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 404 : pppp17-{T}(E7,E7,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 405 : subactivity_occurrence-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 406 : root-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 407 : subactivity-{T}(E7,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 408 : pppp3-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 409 : pppp4-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 410 : pppp33-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 411 : atocc-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 412 : root_occ-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 413 : pppp19-{T}(E1,E7,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 414 : pppp14-{T}(E1,E7,E4) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 415 : pppp1-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 416 : subactivity-{T}(E7,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 417 : leaf-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 418 : pppp35-{T}(E7,E6) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 15, 21, 27, 34, 37, 44, 59, 76 }
% 28.24/28.41 419 : pppp5-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 420 : leaf_occ-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 421 : pppp20-{T}(E1,E7,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76 }
% 28.24/28.41 422 : pppp36-{T}(E1,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76, 77 }
% 28.24/28.41 423 : pppp9-{T}(E1,E7,E2) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76, 78 }
% 28.24/28.41 424 : subactivity-{T}(E2,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76, 78 }
% 28.24/28.41 425 : pppp35-{T}(E4,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76, 78 }
% 28.24/28.41 426 : pppp16-{T}(E1,E7,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76, 79 }
% 28.24/28.41 427 : pppp18-{T}(E7,E6,E0) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 15, 21, 27, 34, 37, 44, 59, 76, 80 }
% 28.24/28.41 428 : pppp21-{T}(E1,E7,E7) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76, 77, 81 }
% 28.24/28.41 429 : pppp18-{T}(E4,E7,E1) { 0, 1, 2, 3, 4, 5, 6, 7, 10, 15, 34, 59, 76, 78, 82 }
% 28.24/28.41
% 28.24/28.41
% 28.24/28.41 % SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.24/28.41
% 28.24/28.41 randbase = 1
%------------------------------------------------------------------------------