%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : GEO355+1 : TPTP v8.1.0. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n021.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:02:29 EDT 2022
% Result : Satisfiable 5.31s 5.49s
% Output : Model 5.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO355+1 : TPTP v8.1.0. Released v6.4.0.
% 0.06/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.12/0.33 % Computer : n021.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 17:40:48 EDT 2022
% 0.12/0.33 % CPUTime :
% 5.31/5.49 GeoParameters:
% 5.31/5.49
% 5.31/5.49 tptp_input = 1
% 5.31/5.49 tptp_output = 0
% 5.31/5.49 nonempty = 1
% 5.31/5.49 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.31/5.49 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 5.31/5.49
% 5.31/5.49
% 5.31/5.49 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.31/5.49 % SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.31/5.49
% 5.31/5.49 Interpretation 23:
% 5.31/5.49 Guesses:
% 5.31/5.49 0 : guesser 4, 3, ( | 1, 0 ), 0, 5s old, 0 lemmas
% 5.31/5.49 1 : guesser 33, 31, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 5.31/5.49 2 : guesser 36, 34, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 5.31/5.49 3 : guesser 37, 35, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 5.31/5.49 4 : guesser 38, 36, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 5.31/5.49 5 : guesser 41, 39, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 5.31/5.49 6 : guesser 44, 42, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 5.31/5.49 7 : guesser 47, 45, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 5.31/5.49 8 : guesser 50, 48, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 5.31/5.49 9 : guesser 51, 49, ( 1 | 2, 0 ), 7, 4s old, 1 lemmas
% 5.31/5.49 10 : guesser 146, 143, ( | 0, 2, 3, 1 ), 8, 4s old, 0 lemmas
% 5.31/5.49 11 : guesser 147, 144, ( 0, 2 | 3, 1 ), 8, 4s old, 1 lemmas
% 5.31/5.49 12 : guesser 370, 366, ( | 1, 0, 3, 4, 2 ), 9, 4s old, 0 lemmas
% 5.31/5.49 13 : guesser 371, 367, ( 2 | 1, 0, 4, 3 ), 9, 4s old, 1 lemmas
% 5.31/5.49 14 : guesser 372, 368, ( | 3, 2, 1, 4, 0 ), 10, 4s old, 0 lemmas
% 5.31/5.49 15 : guesser 378, 374, ( | 0, 1 ), 19, 0s old, 0 lemmas
% 5.31/5.49 16 : guesser 382, 378, ( | 1, 0, 3, 4, 2 ), 19, 0s old, 0 lemmas
% 5.31/5.49 17 : guesser 387, 383, ( | 0, 3, 2, 4, 1 ), 19, 0s old, 0 lemmas
% 5.31/5.49 18 : guesser 392, 388, ( | 2, 1, 0, 4, 3 ), 19, 0s old, 0 lemmas
% 5.31/5.49 19 : guesser 397, 393, ( | 3, 2, 1, 4, 0 ), 19, 0s old, 0 lemmas
% 5.31/5.49 20 : guesser 402, 398, ( | 3, 2, 1, 4, 0 ), 19, 0s old, 0 lemmas
% 5.31/5.49 21 : guesser 407, 403, ( | 1, 0, 3, 4, 2 ), 19, 0s old, 0 lemmas
% 5.31/5.49 22 : guesser 408, 404, ( | 2, 1, 0, 4, 3 ), 19, 0s old, 0 lemmas
% 5.31/5.49 23 : guesser 409, 405, ( 3 | 2, 1, 4, 0 ), 19, 0s old, 1 lemmas
% 5.31/5.49 24 : guesser 414, 410, ( | 2, 1, 0, 4, 3 ), 20, 0s old, 0 lemmas
% 5.31/5.49 25 : guesser 415, 411, ( | 1, 0, 3, 4, 2 ), 20, 0s old, 0 lemmas
% 5.31/5.49 26 : guesser 416, 412, ( | 0, 1 ), 20, 0s old, 0 lemmas
% 5.31/5.49 27 : guesser 417, 413, ( | 2, 1, 0, 4, 3 ), 20, 0s old, 0 lemmas
% 5.31/5.50 28 : guesser 418, 414, ( | 2, 1, 0, 4, 3 ), 20, 0s old, 0 lemmas
% 5.31/5.50 29 : guesser 419, 415, ( | 0, 3, 2, 4, 1 ), 20, 0s old, 0 lemmas
% 5.31/5.50 30 : guesser 424, 420, ( | 0, 3, 2, 4, 1 ), 20, 0s old, 0 lemmas
% 5.31/5.50 31 : guesser 425, 421, ( | 2, 1, 0, 4, 3 ), 20, 0s old, 0 lemmas
% 5.31/5.50 32 : guesser 426, 422, ( | 2, 1, 0, 4, 3 ), 20, 0s old, 0 lemmas
% 5.31/5.50 33 : guesser 431, 427, ( | 2, 1, 0, 4, 3 ), 20, 0s old, 0 lemmas
% 5.31/5.50 34 : guesser 432, 428, ( | 2, 1, 0, 4, 3 ), 20, 0s old, 0 lemmas
% 5.31/5.50 35 : guesser 433, 429, ( | 3, 2, 1, 4, 0 ), 20, 0s old, 0 lemmas
% 5.31/5.50 36 : guesser 438, 434, ( | 2, 1, 0, 4, 3 ), 20, 0s old, 0 lemmas
% 5.31/5.50 37 : guesser 443, 439, ( | 2, 1, 0, 4, 3 ), 20, 0s old, 0 lemmas
% 5.31/5.50 38 : guesser 448, 444, ( | 3, 2, 1, 4, 0 ), 20, 0s old, 0 lemmas
% 5.31/5.50 39 : guesser 449, 445, ( 1 | 0, 3, 4, 2 ), 20, 0s old, 1 lemmas
% 5.31/5.50 40 : guesser 450, 446, ( | 0, 3, 2, 4, 1 ), 21, 0s old, 0 lemmas
% 5.31/5.50 41 : guesser 451, 447, ( | 3, 2, 1, 4, 0 ), 21, 0s old, 0 lemmas
% 5.31/5.50 42 : guesser 452, 448, ( | 3, 2, 1, 4, 0 ), 21, 0s old, 0 lemmas
% 5.31/5.50 43 : guesser 457, 453, ( | 1, 0, 3, 4, 2 ), 21, 0s old, 0 lemmas
% 5.31/5.50 44 : guesser 458, 454, ( 0 | 3, 2, 4, 1 ), 21, 0s old, 1 lemmas
% 5.31/5.50 45 : guesser 459, 455, ( | 3, 2, 1, 4, 0 ), 22, 0s old, 0 lemmas
% 5.31/5.50 46 : guesser 460, 456, ( 0 | 3, 2, 4, 1 ), 22, 0s old, 1 lemmas
% 5.31/5.50 47 : guesser 461, 457, ( | 0, 3, 2, 4, 1 ), 23, 0s old, 0 lemmas
% 5.31/5.50 48 : guesser 462, 458, ( | 3, 2, 1, 4, 0 ), 23, 0s old, 0 lemmas
% 5.31/5.50 49 : guesser 463, 459, ( | 3, 2, 1, 4, 0 ), 23, 0s old, 0 lemmas
% 5.31/5.50 50 : guesser 468, 464, ( | 1, 0, 3, 4, 2 ), 23, 0s old, 0 lemmas
% 5.31/5.50 51 : guesser 469, 465, ( | 2, 1, 0, 4, 3 ), 23, 0s old, 0 lemmas
% 5.31/5.50 52 : guesser 470, 466, ( | 2, 1, 0, 4, 3 ), 23, 0s old, 0 lemmas
% 5.31/5.50 53 : guesser 471, 467, ( | 3, 2, 1, 4, 0 ), 23, 0s old, 0 lemmas
% 5.31/5.50
% 5.31/5.50 Elements:
% 5.31/5.50 { E0, E1, E2, E3 }
% 5.31/5.50
% 5.31/5.50 Atoms:
% 5.31/5.50 0 : #-{T} E0 { }
% 5.31/5.50 1 : equally_directed_lines-{T}(E0,E0) { }
% 5.31/5.50 2 : pppp5-{T}(E0,E0,E0) { }
% 5.31/5.50 3 : pppp7-{T}(E0,E0,E0,E0) { }
% 5.31/5.50 4 : #-{T} E1 { 0 }
% 5.31/5.50 5 : P_reverse_line-{T}(E0,E1) { 0 }
% 5.31/5.50 6 : equally_directed_lines-{T}(E1,E1) { 0 }
% 5.31/5.50 7 : pppp5-{T}(E0,E0,E1) { 0 }
% 5.31/5.50 8 : pppp7-{T}(E0,E0,E0,E1) { 0 }
% 5.31/5.50 9 : pppp5-{T}(E0,E1,E1) { 0 }
% 5.31/5.50 10 : pppp7-{T}(E0,E0,E1,E1) { 0 }
% 5.31/5.50 11 : pppp5-{T}(E0,E1,E0) { 0 }
% 5.31/5.50 12 : pppp7-{T}(E0,E0,E1,E0) { 0 }
% 5.31/5.50 13 : pppp5-{T}(E1,E0,E0) { 0 }
% 5.31/5.50 14 : pppp7-{T}(E0,E1,E0,E0) { 0 }
% 5.31/5.50 15 : pppp5-{T}(E1,E0,E1) { 0 }
% 5.31/5.50 16 : pppp7-{T}(E0,E1,E0,E1) { 0 }
% 5.31/5.50 17 : pppp5-{T}(E1,E1,E1) { 0 }
% 5.31/5.50 18 : pppp7-{T}(E0,E1,E1,E1) { 0 }
% 5.31/5.50 19 : pppp5-{T}(E1,E1,E0) { 0 }
% 5.31/5.50 20 : pppp7-{T}(E0,E1,E1,E0) { 0 }
% 5.31/5.50 21 : pppp7-{T}(E1,E0,E0,E0) { 0 }
% 5.31/5.50 22 : pppp7-{T}(E1,E0,E0,E1) { 0 }
% 5.31/5.50 23 : pppp7-{T}(E1,E0,E1,E1) { 0 }
% 5.31/5.50 24 : pppp7-{T}(E1,E0,E1,E0) { 0 }
% 5.31/5.50 25 : pppp7-{T}(E1,E1,E0,E0) { 0 }
% 5.31/5.50 26 : pppp7-{T}(E1,E1,E0,E1) { 0 }
% 5.31/5.50 27 : pppp7-{T}(E1,E1,E1,E1) { 0 }
% 5.31/5.50 28 : pppp7-{T}(E1,E1,E1,E0) { 0 }
% 5.31/5.50 29 : equally_directed_opposite_lines-{T}(E1,E0) { 0 }
% 5.31/5.50 30 : unequally_directed_lines-{T}(E0,E1) { 0 }
% 5.31/5.50 31 : unequally_directed_opposite_lines-{T}(E0,E0) { 0 }
% 5.31/5.50 32 : unequally_directed_lines-{T}(E1,E0) { 0 }
% 5.31/5.50 33 : P_line_connecting-{T}(E0,E0,E1) { 1 }
% 5.31/5.50 34 : pppp6-{T}(E0,E0,E0,E1) { 1 }
% 5.31/5.50 35 : pppp6-{T}(E0,E1,E0,E1) { 0, 1 }
% 5.31/5.50 36 : P_intersection_point-{T}(E0,E0,E0) { 2 }
% 5.31/5.50 37 : P_parallel_through_point-{T}(E0,E0,E0) { 3 }
% 5.31/5.50 38 : P_reverse_line-{T}(E1,E0) { 0, 4 }
% 5.31/5.50 39 : unequally_directed_opposite_lines-{T}(E1,E1) { 0, 4 }
% 5.31/5.50 40 : equally_directed_opposite_lines-{T}(E0,E1) { 0, 4 }
% 5.31/5.50 41 : P_line_connecting-{T}(E0,E1,E0) { 0, 5 }
% 5.31/5.50 42 : pppp6-{T}(E0,E0,E1,E0) { 0, 5 }
% 5.31/5.50 43 : pppp6-{T}(E0,E1,E1,E0) { 0, 5 }
% 5.31/5.50 44 : P_line_connecting-{T}(E1,E1,E0) { 0, 6 }
% 5.31/5.50 45 : pppp6-{T}(E1,E0,E1,E0) { 0, 6 }
% 5.31/5.50 46 : pppp6-{T}(E1,E1,E1,E0) { 0, 6 }
% 5.31/5.50 47 : P_line_connecting-{T}(E1,E0,E0) { 0, 7 }
% 5.31/5.50 48 : pppp6-{T}(E1,E0,E0,E0) { 0, 7 }
% 5.31/5.50 49 : pppp6-{T}(E1,E1,E0,E0) { 0, 7 }
% 5.31/5.50 50 : P_intersection_point-{T}(E0,E1,E1) { 0, 8 }
% 5.31/5.50 51 : #-{T} E2 { 0, 9 }
% 5.31/5.50 52 : P_parallel_through_point-{T}(E0,E1,E2) { 0, 9 }
% 5.31/5.50 53 : equally_directed_lines-{T}(E2,E2) { 0, 9 }
% 5.31/5.50 54 : equally_directed_lines-{T}(E2,E0) { 0, 9 }
% 5.31/5.50 55 : pppp5-{T}(E0,E0,E2) { 0, 9 }
% 5.31/5.50 56 : unequally_directed_lines-{T}(E2,E1) { 0, 9 }
% 5.31/5.50 57 : pppp5-{T}(E0,E1,E2) { 0, 9 }
% 5.31/5.50 58 : pppp7-{T}(E0,E0,E0,E2) { 0, 9 }
% 5.31/5.50 59 : unequally_directed_opposite_lines-{T}(E2,E0) { 0, 9 }
% 5.31/5.50 60 : pppp5-{T}(E0,E2,E2) { 0, 9 }
% 5.31/5.50 61 : pppp7-{T}(E0,E0,E1,E2) { 0, 9 }
% 5.31/5.50 62 : pppp5-{T}(E0,E2,E1) { 0, 9 }
% 5.31/5.50 63 : pppp7-{T}(E0,E0,E2,E2) { 0, 9 }
% 5.31/5.50 64 : pppp6-{T}(E0,E2,E0,E1) { 0, 1, 9 }
% 5.31/5.50 65 : pppp5-{T}(E0,E2,E0) { 0, 9 }
% 5.31/5.50 66 : pppp7-{T}(E0,E0,E2,E1) { 0, 9 }
% 5.31/5.50 67 : equally_directed_opposite_lines-{T}(E2,E1) { 0, 4, 9 }
% 5.31/5.50 68 : pppp5-{T}(E1,E0,E2) { 0, 9 }
% 5.31/5.50 69 : pppp7-{T}(E0,E0,E2,E0) { 0, 9 }
% 5.31/5.50 70 : pppp6-{T}(E0,E2,E1,E0) { 0, 5, 9 }
% 5.31/5.50 71 : pppp5-{T}(E1,E1,E2) { 0, 9 }
% 5.31/5.50 72 : pppp7-{T}(E0,E1,E0,E2) { 0, 9 }
% 5.31/5.50 73 : pppp6-{T}(E1,E2,E1,E0) { 0, 6, 9 }
% 5.31/5.50 74 : pppp5-{T}(E1,E2,E2) { 0, 9 }
% 5.31/5.50 75 : pppp7-{T}(E0,E1,E1,E2) { 0, 9 }
% 5.31/5.50 76 : pppp6-{T}(E1,E2,E0,E0) { 0, 7, 9 }
% 5.31/5.50 77 : pppp5-{T}(E1,E2,E1) { 0, 9 }
% 5.31/5.50 78 : pppp7-{T}(E0,E1,E2,E2) { 0, 9 }
% 5.31/5.50 79 : pppp5-{T}(E1,E2,E0) { 0, 9 }
% 5.31/5.50 80 : pppp7-{T}(E0,E1,E2,E1) { 0, 9 }
% 5.31/5.50 81 : pppp5-{T}(E2,E0,E0) { 0, 9 }
% 5.31/5.50 82 : pppp7-{T}(E0,E1,E2,E0) { 0, 9 }
% 5.31/5.50 83 : pppp5-{T}(E2,E0,E2) { 0, 9 }
% 5.31/5.50 84 : pppp7-{T}(E0,E2,E0,E0) { 0, 9 }
% 5.31/5.50 85 : pppp5-{T}(E2,E0,E1) { 0, 9 }
% 5.31/5.50 86 : pppp7-{T}(E0,E2,E0,E2) { 0, 9 }
% 5.31/5.50 87 : pppp5-{T}(E2,E1,E1) { 0, 9 }
% 5.31/5.50 88 : pppp7-{T}(E0,E2,E0,E1) { 0, 9 }
% 5.31/5.50 89 : pppp5-{T}(E2,E1,E0) { 0, 9 }
% 5.31/5.50 90 : pppp7-{T}(E0,E2,E1,E1) { 0, 9 }
% 5.31/5.50 91 : pppp5-{T}(E2,E1,E2) { 0, 9 }
% 5.31/5.50 92 : pppp7-{T}(E0,E2,E1,E0) { 0, 9 }
% 5.31/5.50 93 : pppp5-{T}(E2,E2,E2) { 0, 9 }
% 5.31/5.50 94 : pppp7-{T}(E0,E2,E1,E2) { 0, 9 }
% 5.31/5.50 95 : pppp5-{T}(E2,E2,E1) { 0, 9 }
% 5.31/5.50 96 : pppp7-{T}(E0,E2,E2,E2) { 0, 9 }
% 5.31/5.50 97 : pppp5-{T}(E2,E2,E0) { 0, 9 }
% 5.31/5.50 98 : pppp7-{T}(E0,E2,E2,E1) { 0, 9 }
% 5.31/5.50 99 : pppp7-{T}(E0,E2,E2,E0) { 0, 9 }
% 5.31/5.50 100 : pppp7-{T}(E1,E0,E0,E2) { 0, 9 }
% 5.31/5.50 101 : pppp7-{T}(E1,E0,E1,E2) { 0, 9 }
% 5.31/5.50 102 : pppp7-{T}(E1,E0,E2,E2) { 0, 9 }
% 5.31/5.50 103 : pppp7-{T}(E1,E0,E2,E1) { 0, 9 }
% 5.31/5.50 104 : pppp7-{T}(E1,E0,E2,E0) { 0, 9 }
% 5.31/5.50 105 : pppp7-{T}(E1,E1,E0,E2) { 0, 9 }
% 5.31/5.50 106 : pppp7-{T}(E1,E1,E1,E2) { 0, 9 }
% 5.31/5.50 107 : pppp7-{T}(E1,E1,E2,E2) { 0, 9 }
% 5.31/5.50 108 : pppp7-{T}(E1,E1,E2,E1) { 0, 9 }
% 5.31/5.50 109 : pppp7-{T}(E1,E1,E2,E0) { 0, 9 }
% 5.31/5.50 110 : pppp7-{T}(E1,E2,E0,E0) { 0, 9 }
% 5.31/5.50 111 : pppp7-{T}(E1,E2,E0,E2) { 0, 9 }
% 5.31/5.50 112 : pppp7-{T}(E1,E2,E0,E1) { 0, 9 }
% 5.31/5.50 113 : pppp7-{T}(E1,E2,E1,E1) { 0, 9 }
% 5.31/5.50 114 : pppp7-{T}(E1,E2,E1,E0) { 0, 9 }
% 5.31/5.50 115 : pppp7-{T}(E1,E2,E1,E2) { 0, 9 }
% 5.31/5.50 116 : pppp7-{T}(E1,E2,E2,E2) { 0, 9 }
% 5.31/5.50 117 : pppp7-{T}(E1,E2,E2,E1) { 0, 9 }
% 5.31/5.50 118 : pppp7-{T}(E1,E2,E2,E0) { 0, 9 }
% 5.31/5.50 119 : pppp7-{T}(E2,E0,E0,E0) { 0, 9 }
% 5.31/5.50 120 : pppp7-{T}(E2,E0,E0,E2) { 0, 9 }
% 5.31/5.50 121 : pppp7-{T}(E2,E0,E0,E1) { 0, 9 }
% 5.31/5.50 122 : pppp7-{T}(E2,E0,E1,E1) { 0, 9 }
% 5.31/5.50 123 : pppp7-{T}(E2,E0,E1,E0) { 0, 9 }
% 5.31/5.50 124 : pppp7-{T}(E2,E0,E1,E2) { 0, 9 }
% 5.31/5.50 125 : pppp7-{T}(E2,E0,E2,E2) { 0, 9 }
% 5.31/5.50 126 : pppp7-{T}(E2,E0,E2,E1) { 0, 9 }
% 5.31/5.50 127 : pppp7-{T}(E2,E0,E2,E0) { 0, 9 }
% 5.31/5.50 128 : pppp7-{T}(E2,E1,E0,E0) { 0, 9 }
% 5.31/5.50 129 : pppp7-{T}(E2,E1,E0,E2) { 0, 9 }
% 5.31/5.50 130 : pppp7-{T}(E2,E1,E0,E1) { 0, 9 }
% 5.31/5.50 131 : pppp7-{T}(E2,E1,E1,E1) { 0, 9 }
% 5.31/5.50 132 : pppp7-{T}(E2,E1,E1,E0) { 0, 9 }
% 5.31/5.50 133 : pppp7-{T}(E2,E1,E1,E2) { 0, 9 }
% 5.31/5.50 134 : pppp7-{T}(E2,E1,E2,E2) { 0, 9 }
% 5.31/5.50 135 : pppp7-{T}(E2,E1,E2,E1) { 0, 9 }
% 5.31/5.50 136 : pppp7-{T}(E2,E1,E2,E0) { 0, 9 }
% 5.31/5.50 137 : pppp7-{T}(E2,E2,E0,E0) { 0, 9 }
% 5.31/5.50 138 : pppp7-{T}(E2,E2,E0,E2) { 0, 9 }
% 5.31/5.50 139 : pppp7-{T}(E2,E2,E0,E1) { 0, 9 }
% 5.31/5.50 140 : pppp7-{T}(E2,E2,E1,E1) { 0, 9 }
% 5.31/5.50 141 : pppp7-{T}(E2,E2,E1,E0) { 0, 9 }
% 5.31/5.50 142 : pppp7-{T}(E2,E2,E1,E2) { 0, 9 }
% 5.31/5.50 143 : pppp7-{T}(E2,E2,E2,E2) { 0, 9 }
% 5.31/5.50 144 : pppp7-{T}(E2,E2,E2,E1) { 0, 9 }
% 5.31/5.50 145 : pppp7-{T}(E2,E2,E2,E0) { 0, 9 }
% 5.31/5.50 146 : P_intersection_point-{T}(E1,E1,E0) { 0, 10 }
% 5.31/5.50 147 : #-{T} E3 { 0, 11 }
% 5.31/5.50 148 : P_parallel_through_point-{T}(E1,E1,E3) { 0, 11 }
% 5.31/5.50 149 : equally_directed_lines-{T}(E3,E3) { 0, 11 }
% 5.31/5.50 150 : equally_directed_lines-{T}(E3,E1) { 0, 11 }
% 5.31/5.50 151 : pppp5-{T}(E0,E0,E3) { 0, 11 }
% 5.31/5.50 152 : equally_directed_opposite_lines-{T}(E3,E0) { 0, 11 }
% 5.31/5.50 153 : unequally_directed_lines-{T}(E3,E0) { 0, 11 }
% 5.31/5.50 154 : pppp5-{T}(E0,E1,E3) { 0, 11 }
% 5.31/5.50 155 : pppp5-{T}(E0,E3,E1) { 0, 11 }
% 5.31/5.50 156 : pppp7-{T}(E0,E0,E0,E3) { 0, 11 }
% 5.31/5.50 157 : pppp6-{T}(E0,E3,E0,E1) { 0, 1, 11 }
% 5.31/5.50 158 : pppp5-{T}(E0,E3,E0) { 0, 11 }
% 5.31/5.50 159 : pppp7-{T}(E0,E0,E1,E3) { 0, 11 }
% 5.31/5.50 160 : unequally_directed_opposite_lines-{T}(E3,E1) { 0, 4, 11 }
% 5.31/5.50 161 : pppp5-{T}(E0,E3,E3) { 0, 11 }
% 5.31/5.50 162 : pppp7-{T}(E0,E0,E3,E1) { 0, 11 }
% 5.31/5.50 163 : pppp6-{T}(E0,E3,E1,E0) { 0, 5, 11 }
% 5.31/5.50 164 : pppp5-{T}(E1,E0,E3) { 0, 11 }
% 5.31/5.50 165 : pppp7-{T}(E0,E0,E3,E0) { 0, 11 }
% 5.31/5.50 166 : pppp6-{T}(E1,E3,E1,E0) { 0, 6, 11 }
% 5.31/5.50 167 : pppp5-{T}(E1,E1,E3) { 0, 11 }
% 5.31/5.50 168 : pppp7-{T}(E0,E0,E3,E3) { 0, 11 }
% 5.31/5.50 169 : pppp6-{T}(E1,E3,E0,E0) { 0, 7, 11 }
% 5.31/5.50 170 : pppp5-{T}(E1,E3,E1) { 0, 11 }
% 5.31/5.50 171 : pppp7-{T}(E0,E1,E0,E3) { 0, 11 }
% 5.31/5.50 172 : pppp5-{T}(E1,E3,E0) { 0, 11 }
% 5.31/5.50 173 : pppp7-{T}(E0,E1,E1,E3) { 0, 11 }
% 5.31/5.50 174 : pppp5-{T}(E1,E3,E3) { 0, 11 }
% 5.31/5.50 175 : pppp7-{T}(E0,E1,E3,E1) { 0, 11 }
% 5.31/5.50 176 : pppp5-{T}(E3,E0,E3) { 0, 11 }
% 5.31/5.50 177 : pppp7-{T}(E0,E1,E3,E0) { 0, 11 }
% 5.31/5.50 178 : pppp5-{T}(E3,E0,E1) { 0, 11 }
% 5.31/5.50 179 : pppp7-{T}(E0,E1,E3,E3) { 0, 11 }
% 5.31/5.50 180 : pppp5-{T}(E3,E0,E0) { 0, 11 }
% 5.31/5.50 181 : pppp7-{T}(E0,E3,E0,E3) { 0, 11 }
% 5.31/5.50 182 : pppp5-{T}(E3,E1,E0) { 0, 11 }
% 5.31/5.50 183 : pppp7-{T}(E0,E3,E0,E1) { 0, 11 }
% 5.31/5.50 184 : pppp5-{T}(E3,E1,E3) { 0, 11 }
% 5.31/5.50 185 : pppp7-{T}(E0,E3,E0,E0) { 0, 11 }
% 5.31/5.50 186 : pppp5-{T}(E3,E1,E1) { 0, 11 }
% 5.31/5.50 187 : pppp7-{T}(E0,E3,E1,E0) { 0, 11 }
% 5.31/5.50 188 : pppp5-{T}(E3,E3,E1) { 0, 11 }
% 5.31/5.50 189 : pppp7-{T}(E0,E3,E1,E3) { 0, 11 }
% 5.31/5.50 190 : pppp5-{T}(E3,E3,E0) { 0, 11 }
% 5.31/5.50 191 : pppp7-{T}(E0,E3,E1,E1) { 0, 11 }
% 5.31/5.50 192 : pppp5-{T}(E3,E3,E3) { 0, 11 }
% 5.31/5.50 193 : pppp7-{T}(E0,E3,E3,E1) { 0, 11 }
% 5.31/5.50 194 : pppp7-{T}(E0,E3,E3,E0) { 0, 11 }
% 5.31/5.50 195 : pppp5-{T}(E0,E2,E3) { 0, 9, 11 }
% 5.31/5.50 196 : pppp7-{T}(E0,E3,E3,E3) { 0, 11 }
% 5.31/5.50 197 : pppp5-{T}(E0,E3,E2) { 0, 9, 11 }
% 5.31/5.50 198 : pppp7-{T}(E1,E0,E0,E3) { 0, 11 }
% 5.31/5.50 199 : pppp5-{T}(E1,E2,E3) { 0, 9, 11 }
% 5.31/5.50 200 : pppp7-{T}(E1,E0,E1,E3) { 0, 11 }
% 5.31/5.50 201 : pppp5-{T}(E1,E3,E2) { 0, 9, 11 }
% 5.31/5.50 202 : pppp7-{T}(E1,E0,E3,E1) { 0, 11 }
% 5.31/5.50 203 : pppp5-{T}(E2,E0,E3) { 0, 9, 11 }
% 5.31/5.50 204 : pppp7-{T}(E1,E0,E3,E0) { 0, 11 }
% 5.31/5.50 205 : pppp5-{T}(E2,E1,E3) { 0, 9, 11 }
% 5.31/5.50 206 : pppp7-{T}(E1,E0,E3,E3) { 0, 11 }
% 5.31/5.50 207 : pppp5-{T}(E2,E2,E3) { 0, 9, 11 }
% 5.31/5.50 208 : pppp7-{T}(E1,E1,E0,E3) { 0, 11 }
% 5.31/5.50 209 : pppp5-{T}(E2,E3,E3) { 0, 9, 11 }
% 5.31/5.50 210 : pppp7-{T}(E1,E1,E1,E3) { 0, 11 }
% 5.31/5.50 211 : pppp5-{T}(E2,E3,E2) { 0, 9, 11 }
% 5.31/5.50 212 : pppp7-{T}(E1,E1,E3,E1) { 0, 11 }
% 5.31/5.50 213 : pppp5-{T}(E2,E3,E1) { 0, 9, 11 }
% 5.31/5.50 214 : pppp7-{T}(E1,E1,E3,E0) { 0, 11 }
% 5.31/5.50 215 : pppp5-{T}(E2,E3,E0) { 0, 9, 11 }
% 5.31/5.50 216 : pppp7-{T}(E1,E1,E3,E3) { 0, 11 }
% 5.31/5.50 217 : pppp5-{T}(E3,E0,E2) { 0, 9, 11 }
% 5.31/5.50 218 : pppp7-{T}(E1,E3,E0,E3) { 0, 11 }
% 5.31/5.50 219 : pppp5-{T}(E3,E1,E2) { 0, 9, 11 }
% 5.31/5.50 220 : pppp7-{T}(E1,E3,E0,E1) { 0, 11 }
% 5.31/5.50 221 : pppp5-{T}(E3,E2,E2) { 0, 9, 11 }
% 5.31/5.50 222 : pppp7-{T}(E1,E3,E0,E0) { 0, 11 }
% 5.31/5.50 223 : pppp5-{T}(E3,E2,E1) { 0, 9, 11 }
% 5.31/5.50 224 : pppp7-{T}(E1,E3,E1,E0) { 0, 11 }
% 5.31/5.50 225 : pppp5-{T}(E3,E2,E0) { 0, 9, 11 }
% 5.31/5.50 226 : pppp7-{T}(E1,E3,E1,E3) { 0, 11 }
% 5.31/5.50 227 : pppp5-{T}(E3,E2,E3) { 0, 9, 11 }
% 5.31/5.50 228 : pppp7-{T}(E1,E3,E1,E1) { 0, 11 }
% 5.31/5.50 229 : pppp5-{T}(E3,E3,E2) { 0, 9, 11 }
% 5.31/5.50 230 : pppp7-{T}(E1,E3,E3,E1) { 0, 11 }
% 5.31/5.50 231 : pppp7-{T}(E1,E3,E3,E0) { 0, 11 }
% 5.31/5.50 232 : pppp7-{T}(E1,E3,E3,E3) { 0, 11 }
% 5.31/5.50 233 : pppp7-{T}(E3,E0,E0,E3) { 0, 11 }
% 5.31/5.50 234 : pppp7-{T}(E3,E0,E0,E1) { 0, 11 }
% 5.31/5.50 235 : pppp7-{T}(E3,E0,E0,E0) { 0, 11 }
% 5.31/5.50 236 : pppp7-{T}(E3,E0,E1,E0) { 0, 11 }
% 5.31/5.50 237 : pppp7-{T}(E3,E0,E1,E3) { 0, 11 }
% 5.31/5.50 238 : pppp7-{T}(E3,E0,E1,E1) { 0, 11 }
% 5.31/5.50 239 : pppp7-{T}(E3,E0,E3,E1) { 0, 11 }
% 5.31/5.50 240 : pppp7-{T}(E3,E0,E3,E0) { 0, 11 }
% 5.31/5.50 241 : pppp7-{T}(E3,E0,E3,E3) { 0, 11 }
% 5.31/5.50 242 : pppp7-{T}(E3,E1,E0,E3) { 0, 11 }
% 5.31/5.50 243 : pppp7-{T}(E3,E1,E0,E1) { 0, 11 }
% 5.31/5.50 244 : pppp7-{T}(E3,E1,E0,E0) { 0, 11 }
% 5.31/5.50 245 : pppp7-{T}(E3,E1,E1,E0) { 0, 11 }
% 5.31/5.50 246 : pppp7-{T}(E3,E1,E1,E3) { 0, 11 }
% 5.31/5.50 247 : pppp7-{T}(E3,E1,E1,E1) { 0, 11 }
% 5.31/5.50 248 : pppp7-{T}(E3,E1,E3,E1) { 0, 11 }
% 5.31/5.50 249 : pppp7-{T}(E3,E1,E3,E0) { 0, 11 }
% 5.31/5.50 250 : pppp7-{T}(E3,E1,E3,E3) { 0, 11 }
% 5.31/5.50 251 : pppp7-{T}(E3,E3,E0,E3) { 0, 11 }
% 5.31/5.50 252 : pppp7-{T}(E3,E3,E0,E1) { 0, 11 }
% 5.31/5.50 253 : pppp7-{T}(E3,E3,E0,E0) { 0, 11 }
% 5.31/5.50 254 : pppp7-{T}(E3,E3,E1,E0) { 0, 11 }
% 5.31/5.50 255 : pppp7-{T}(E3,E3,E1,E3) { 0, 11 }
% 5.31/5.50 256 : pppp7-{T}(E3,E3,E1,E1) { 0, 11 }
% 5.31/5.50 257 : pppp7-{T}(E3,E3,E3,E1) { 0, 11 }
% 5.31/5.50 258 : pppp7-{T}(E3,E3,E3,E0) { 0, 11 }
% 5.31/5.50 259 : pppp7-{T}(E3,E3,E3,E3) { 0, 11 }
% 5.31/5.50 260 : pppp7-{T}(E0,E0,E2,E3) { 0, 9, 11 }
% 5.31/5.50 261 : pppp7-{T}(E0,E0,E3,E2) { 0, 9, 11 }
% 5.31/5.50 262 : pppp7-{T}(E0,E1,E2,E3) { 0, 9, 11 }
% 5.31/5.50 263 : pppp7-{T}(E0,E1,E3,E2) { 0, 9, 11 }
% 5.31/5.50 264 : pppp7-{T}(E0,E2,E0,E3) { 0, 9, 11 }
% 5.31/5.50 265 : pppp7-{T}(E0,E2,E1,E3) { 0, 9, 11 }
% 5.31/5.50 266 : pppp7-{T}(E0,E2,E2,E3) { 0, 9, 11 }
% 5.31/5.50 267 : pppp7-{T}(E0,E2,E3,E3) { 0, 9, 11 }
% 5.31/5.50 268 : pppp7-{T}(E0,E2,E3,E2) { 0, 9, 11 }
% 5.31/5.50 269 : pppp7-{T}(E0,E2,E3,E1) { 0, 9, 11 }
% 5.31/5.50 270 : pppp7-{T}(E0,E2,E3,E0) { 0, 9, 11 }
% 5.31/5.50 271 : pppp7-{T}(E0,E3,E0,E2) { 0, 9, 11 }
% 5.31/5.50 272 : pppp7-{T}(E0,E3,E1,E2) { 0, 9, 11 }
% 5.31/5.50 273 : pppp7-{T}(E0,E3,E2,E2) { 0, 9, 11 }
% 5.31/5.50 274 : pppp7-{T}(E0,E3,E2,E1) { 0, 9, 11 }
% 5.31/5.50 275 : pppp7-{T}(E0,E3,E2,E0) { 0, 9, 11 }
% 5.31/5.50 276 : pppp7-{T}(E0,E3,E2,E3) { 0, 9, 11 }
% 5.31/5.50 277 : pppp7-{T}(E0,E3,E3,E2) { 0, 9, 11 }
% 5.31/5.50 278 : pppp7-{T}(E1,E0,E2,E3) { 0, 9, 11 }
% 5.31/5.50 279 : pppp7-{T}(E1,E0,E3,E2) { 0, 9, 11 }
% 5.31/5.50 280 : pppp7-{T}(E1,E1,E2,E3) { 0, 9, 11 }
% 5.31/5.50 281 : pppp7-{T}(E1,E1,E3,E2) { 0, 9, 11 }
% 5.31/5.50 282 : pppp7-{T}(E1,E2,E0,E3) { 0, 9, 11 }
% 5.31/5.50 283 : pppp7-{T}(E1,E2,E1,E3) { 0, 9, 11 }
% 5.31/5.50 284 : pppp7-{T}(E1,E2,E2,E3) { 0, 9, 11 }
% 5.31/5.50 285 : pppp7-{T}(E1,E2,E3,E3) { 0, 9, 11 }
% 5.31/5.50 286 : pppp7-{T}(E1,E2,E3,E2) { 0, 9, 11 }
% 5.31/5.50 287 : pppp7-{T}(E1,E2,E3,E1) { 0, 9, 11 }
% 5.31/5.50 288 : pppp7-{T}(E1,E2,E3,E0) { 0, 9, 11 }
% 5.31/5.50 289 : pppp7-{T}(E1,E3,E0,E2) { 0, 9, 11 }
% 5.31/5.50 290 : pppp7-{T}(E1,E3,E1,E2) { 0, 9, 11 }
% 5.31/5.50 291 : pppp7-{T}(E1,E3,E2,E2) { 0, 9, 11 }
% 5.31/5.50 292 : pppp7-{T}(E1,E3,E2,E1) { 0, 9, 11 }
% 5.31/5.50 293 : pppp7-{T}(E1,E3,E2,E0) { 0, 9, 11 }
% 5.31/5.50 294 : pppp7-{T}(E1,E3,E2,E3) { 0, 9, 11 }
% 5.31/5.50 295 : pppp7-{T}(E1,E3,E3,E2) { 0, 9, 11 }
% 5.31/5.50 296 : pppp7-{T}(E2,E0,E0,E3) { 0, 9, 11 }
% 5.31/5.50 297 : pppp7-{T}(E2,E0,E1,E3) { 0, 9, 11 }
% 5.31/5.50 298 : pppp7-{T}(E2,E0,E2,E3) { 0, 9, 11 }
% 5.31/5.50 299 : pppp7-{T}(E2,E0,E3,E3) { 0, 9, 11 }
% 5.31/5.50 300 : pppp7-{T}(E2,E0,E3,E2) { 0, 9, 11 }
% 5.31/5.50 301 : pppp7-{T}(E2,E0,E3,E1) { 0, 9, 11 }
% 5.31/5.50 302 : pppp7-{T}(E2,E0,E3,E0) { 0, 9, 11 }
% 5.31/5.50 303 : pppp7-{T}(E2,E1,E0,E3) { 0, 9, 11 }
% 5.31/5.50 304 : pppp7-{T}(E2,E1,E1,E3) { 0, 9, 11 }
% 5.31/5.50 305 : pppp7-{T}(E2,E1,E2,E3) { 0, 9, 11 }
% 5.31/5.50 306 : pppp7-{T}(E2,E1,E3,E3) { 0, 9, 11 }
% 5.31/5.50 307 : pppp7-{T}(E2,E1,E3,E2) { 0, 9, 11 }
% 5.31/5.50 308 : pppp7-{T}(E2,E1,E3,E1) { 0, 9, 11 }
% 5.31/5.50 309 : pppp7-{T}(E2,E1,E3,E0) { 0, 9, 11 }
% 5.31/5.50 310 : pppp7-{T}(E2,E2,E0,E3) { 0, 9, 11 }
% 5.31/5.50 311 : pppp7-{T}(E2,E2,E1,E3) { 0, 9, 11 }
% 5.31/5.50 312 : pppp7-{T}(E2,E2,E2,E3) { 0, 9, 11 }
% 5.31/5.50 313 : pppp7-{T}(E2,E2,E3,E3) { 0, 9, 11 }
% 5.31/5.50 314 : pppp7-{T}(E2,E2,E3,E2) { 0, 9, 11 }
% 5.31/5.50 315 : pppp7-{T}(E2,E2,E3,E1) { 0, 9, 11 }
% 5.31/5.50 316 : pppp7-{T}(E2,E2,E3,E0) { 0, 9, 11 }
% 5.31/5.50 317 : pppp7-{T}(E2,E3,E0,E0) { 0, 9, 11 }
% 5.31/5.50 318 : pppp7-{T}(E2,E3,E0,E3) { 0, 9, 11 }
% 5.31/5.50 319 : pppp7-{T}(E2,E3,E0,E2) { 0, 9, 11 }
% 5.31/5.50 320 : pppp7-{T}(E2,E3,E0,E1) { 0, 9, 11 }
% 5.31/5.50 321 : pppp7-{T}(E2,E3,E1,E1) { 0, 9, 11 }
% 5.31/5.50 322 : pppp7-{T}(E2,E3,E1,E0) { 0, 9, 11 }
% 5.31/5.50 323 : pppp7-{T}(E2,E3,E1,E3) { 0, 9, 11 }
% 5.31/5.50 324 : pppp7-{T}(E2,E3,E1,E2) { 0, 9, 11 }
% 5.31/5.50 325 : pppp7-{T}(E2,E3,E2,E2) { 0, 9, 11 }
% 5.31/5.50 326 : pppp7-{T}(E2,E3,E2,E1) { 0, 9, 11 }
% 5.31/5.50 327 : pppp7-{T}(E2,E3,E2,E0) { 0, 9, 11 }
% 5.31/5.50 328 : pppp7-{T}(E2,E3,E2,E3) { 0, 9, 11 }
% 5.31/5.50 329 : pppp7-{T}(E2,E3,E3,E3) { 0, 9, 11 }
% 5.31/5.50 330 : pppp7-{T}(E2,E3,E3,E2) { 0, 9, 11 }
% 5.31/5.50 331 : pppp7-{T}(E2,E3,E3,E1) { 0, 9, 11 }
% 5.31/5.50 332 : pppp7-{T}(E2,E3,E3,E0) { 0, 9, 11 }
% 5.31/5.50 333 : pppp7-{T}(E3,E0,E0,E2) { 0, 9, 11 }
% 5.31/5.50 334 : pppp7-{T}(E3,E0,E1,E2) { 0, 9, 11 }
% 5.31/5.50 335 : pppp7-{T}(E3,E0,E2,E2) { 0, 9, 11 }
% 5.31/5.50 336 : pppp7-{T}(E3,E0,E2,E1) { 0, 9, 11 }
% 5.31/5.50 337 : pppp7-{T}(E3,E0,E2,E0) { 0, 9, 11 }
% 5.31/5.50 338 : pppp7-{T}(E3,E0,E2,E3) { 0, 9, 11 }
% 5.31/5.50 339 : pppp7-{T}(E3,E0,E3,E2) { 0, 9, 11 }
% 5.31/5.50 340 : pppp7-{T}(E3,E1,E0,E2) { 0, 9, 11 }
% 5.31/5.50 341 : pppp7-{T}(E3,E1,E1,E2) { 0, 9, 11 }
% 5.31/5.50 342 : pppp7-{T}(E3,E1,E2,E2) { 0, 9, 11 }
% 5.31/5.50 343 : pppp7-{T}(E3,E1,E2,E1) { 0, 9, 11 }
% 5.31/5.50 344 : pppp7-{T}(E3,E1,E2,E0) { 0, 9, 11 }
% 5.31/5.50 345 : pppp7-{T}(E3,E1,E2,E3) { 0, 9, 11 }
% 5.31/5.50 346 : pppp7-{T}(E3,E1,E3,E2) { 0, 9, 11 }
% 5.31/5.50 347 : pppp7-{T}(E3,E2,E0,E0) { 0, 9, 11 }
% 5.31/5.50 348 : pppp7-{T}(E3,E2,E0,E3) { 0, 9, 11 }
% 5.31/5.50 349 : pppp7-{T}(E3,E2,E0,E2) { 0, 9, 11 }
% 5.31/5.50 350 : pppp7-{T}(E3,E2,E0,E1) { 0, 9, 11 }
% 5.31/5.50 351 : pppp7-{T}(E3,E2,E1,E1) { 0, 9, 11 }
% 5.31/5.50 352 : pppp7-{T}(E3,E2,E1,E0) { 0, 9, 11 }
% 5.31/5.50 353 : pppp7-{T}(E3,E2,E1,E3) { 0, 9, 11 }
% 5.31/5.50 354 : pppp7-{T}(E3,E2,E1,E2) { 0, 9, 11 }
% 5.31/5.50 355 : pppp7-{T}(E3,E2,E2,E2) { 0, 9, 11 }
% 5.31/5.50 356 : pppp7-{T}(E3,E2,E2,E1) { 0, 9, 11 }
% 5.31/5.50 357 : pppp7-{T}(E3,E2,E2,E0) { 0, 9, 11 }
% 5.31/5.50 358 : pppp7-{T}(E3,E2,E2,E3) { 0, 9, 11 }
% 5.31/5.50 359 : pppp7-{T}(E3,E2,E3,E3) { 0, 9, 11 }
% 5.31/5.50 360 : pppp7-{T}(E3,E2,E3,E2) { 0, 9, 11 }
% 5.31/5.50 361 : pppp7-{T}(E3,E2,E3,E1) { 0, 9, 11 }
% 5.31/5.50 362 : pppp7-{T}(E3,E2,E3,E0) { 0, 9, 11 }
% 5.31/5.50 363 : pppp7-{T}(E3,E3,E0,E2) { 0, 9, 11 }
% 5.31/5.50 364 : pppp7-{T}(E3,E3,E1,E2) { 0, 9, 11 }
% 5.31/5.50 365 : pppp7-{T}(E3,E3,E2,E2) { 0, 9, 11 }
% 5.31/5.50 366 : pppp7-{T}(E3,E3,E2,E1) { 0, 9, 11 }
% 5.31/5.50 367 : pppp7-{T}(E3,E3,E2,E0) { 0, 9, 11 }
% 5.31/5.50 368 : pppp7-{T}(E3,E3,E2,E3) { 0, 9, 11 }
% 5.31/5.50 369 : pppp7-{T}(E3,E3,E3,E2) { 0, 9, 11 }
% 5.31/5.50 370 : P_intersection_point-{T}(E1,E0,E1) { 0, 12 }
% 5.31/5.50 371 : P_parallel_through_point-{T}(E1,E0,E1) { 0, 13 }
% 5.31/5.50 372 : P_reverse_line-{T}(E2,E3) { 0, 9, 14 }
% 5.31/5.50 373 : unequally_directed_lines-{T}(E2,E3) { 0, 9, 14 }
% 5.31/5.50 374 : equally_directed_opposite_lines-{T}(E3,E2) { 0, 9, 11, 14 }
% 5.31/5.50 375 : unequally_directed_lines-{T}(E3,E2) { 0, 9, 11, 14 }
% 5.31/5.50 376 : unequally_directed_opposite_lines-{T}(E2,E2) { 0, 9, 14 }
% 5.31/5.50 377 : equally_directed_opposite_lines-{T}(E1,E2) { 0, 9, 11, 14 }
% 5.31/5.50 378 : equally_directed_lines-{T}(E0,E2) { 0, 9, 15 }
% 5.31/5.50 379 : unequally_directed_lines-{T}(E0,E3) { 0, 9, 14, 15 }
% 5.31/5.50 380 : unequally_directed_lines-{T}(E1,E2) { 0, 9, 15 }
% 5.31/5.50 381 : unequally_directed_opposite_lines-{T}(E0,E2) { 0, 9, 14, 15 }
% 5.31/5.50 382 : P_line_connecting-{T}(E0,E2,E1) { 0, 9, 16 }
% 5.31/5.50 383 : pppp6-{T}(E0,E0,E2,E1) { 0, 9, 16 }
% 5.31/5.50 384 : pppp6-{T}(E0,E1,E2,E1) { 0, 9, 16 }
% 5.31/5.50 385 : pppp6-{T}(E0,E2,E2,E1) { 0, 9, 16 }
% 5.31/5.50 386 : pppp6-{T}(E0,E3,E2,E1) { 0, 9, 11, 16 }
% 5.31/5.50 387 : P_line_connecting-{T}(E1,E2,E0) { 0, 9, 17 }
% 5.31/5.50 388 : pppp6-{T}(E1,E0,E2,E0) { 0, 9, 17 }
% 5.31/5.50 389 : pppp6-{T}(E1,E1,E2,E0) { 0, 9, 17 }
% 5.31/5.50 390 : pppp6-{T}(E1,E2,E2,E0) { 0, 9, 17 }
% 5.31/5.50 391 : pppp6-{T}(E1,E3,E2,E0) { 0, 9, 11, 17 }
% 5.31/5.50 392 : P_line_connecting-{T}(E2,E1,E2) { 0, 9, 18 }
% 5.31/5.50 393 : pppp6-{T}(E2,E0,E1,E2) { 0, 9, 18 }
% 5.31/5.50 394 : pppp6-{T}(E2,E1,E1,E2) { 0, 9, 18 }
% 5.31/5.50 395 : pppp6-{T}(E2,E2,E1,E2) { 0, 9, 18 }
% 5.31/5.50 396 : pppp6-{T}(E2,E3,E1,E2) { 0, 9, 11, 18 }
% 5.31/5.50 397 : P_line_connecting-{T}(E2,E2,E3) { 0, 9, 19 }
% 5.31/5.50 398 : pppp6-{T}(E2,E0,E2,E3) { 0, 9, 19 }
% 5.31/5.50 399 : pppp6-{T}(E2,E1,E2,E3) { 0, 9, 19 }
% 5.31/5.50 400 : pppp6-{T}(E2,E2,E2,E3) { 0, 9, 19 }
% 5.31/5.50 401 : pppp6-{T}(E2,E3,E2,E3) { 0, 9, 11, 19 }
% 5.31/5.50 402 : P_line_connecting-{T}(E2,E0,E3) { 0, 9, 20 }
% 5.31/5.50 403 : pppp6-{T}(E2,E0,E0,E3) { 0, 9, 20 }
% 5.31/5.50 404 : pppp6-{T}(E2,E1,E0,E3) { 0, 9, 20 }
% 5.31/5.50 405 : pppp6-{T}(E2,E2,E0,E3) { 0, 9, 20 }
% 5.31/5.50 406 : pppp6-{T}(E2,E3,E0,E3) { 0, 9, 11, 20 }
% 5.31/5.50 407 : P_intersection_point-{T}(E0,E2,E1) { 0, 9, 21 }
% 5.31/5.50 408 : P_parallel_through_point-{T}(E0,E2,E2) { 0, 9, 22 }
% 5.31/5.50 409 : P_reverse_line-{T}(E3,E2) { 0, 11, 23 }
% 5.31/5.50 410 : equally_directed_opposite_lines-{T}(E2,E3) { 0, 9, 11, 23 }
% 5.31/5.50 411 : unequally_directed_opposite_lines-{T}(E3,E3) { 0, 9, 11, 14, 23 }
% 5.31/5.50 412 : equally_directed_opposite_lines-{T}(E0,E3) { 0, 9, 11, 23 }
% 5.31/5.50 413 : unequally_directed_opposite_lines-{T}(E1,E3) { 0, 9, 11, 15, 23 }
% 5.31/5.50 414 : P_intersection_point-{T}(E1,E2,E2) { 0, 9, 24 }
% 5.31/5.50 415 : P_parallel_through_point-{T}(E1,E2,E1) { 0, 9, 25 }
% 5.31/5.50 416 : equally_directed_lines-{T}(E1,E3) { 0, 11, 26 }
% 5.31/5.50 417 : P_intersection_point-{T}(E2,E1,E2) { 0, 9, 27 }
% 5.31/5.50 418 : P_parallel_through_point-{T}(E2,E1,E2) { 0, 9, 28 }
% 5.31/5.50 419 : P_line_connecting-{T}(E0,E3,E0) { 0, 11, 29 }
% 5.31/5.50 420 : pppp6-{T}(E0,E0,E3,E0) { 0, 11, 29 }
% 5.31/5.50 421 : pppp6-{T}(E0,E1,E3,E0) { 0, 11, 29 }
% 5.31/5.50 422 : pppp6-{T}(E0,E3,E3,E0) { 0, 11, 29 }
% 5.31/5.50 423 : pppp6-{T}(E0,E2,E3,E0) { 0, 9, 11, 29 }
% 5.31/5.50 424 : P_intersection_point-{T}(E2,E2,E0) { 0, 9, 30 }
% 5.31/5.50 425 : P_parallel_through_point-{T}(E2,E2,E2) { 0, 9, 31 }
% 5.31/5.50 426 : P_line_connecting-{T}(E1,E3,E2) { 0, 11, 32 }
% 5.31/5.50 427 : pppp6-{T}(E1,E0,E3,E2) { 0, 11, 32 }
% 5.31/5.50 428 : pppp6-{T}(E1,E1,E3,E2) { 0, 11, 32 }
% 5.31/5.50 429 : pppp6-{T}(E1,E3,E3,E2) { 0, 11, 32 }
% 5.31/5.50 430 : pppp6-{T}(E1,E2,E3,E2) { 0, 9, 11, 32 }
% 5.31/5.50 431 : P_intersection_point-{T}(E2,E0,E2) { 0, 9, 33 }
% 5.31/5.50 432 : P_parallel_through_point-{T}(E2,E0,E2) { 0, 9, 34 }
% 5.31/5.50 433 : P_line_connecting-{T}(E3,E1,E3) { 0, 11, 35 }
% 5.31/5.50 434 : pppp6-{T}(E3,E0,E1,E3) { 0, 11, 35 }
% 5.31/5.50 435 : pppp6-{T}(E3,E1,E1,E3) { 0, 11, 35 }
% 5.31/5.50 436 : pppp6-{T}(E3,E3,E1,E3) { 0, 11, 35 }
% 5.31/5.50 437 : pppp6-{T}(E3,E2,E1,E3) { 0, 9, 11, 35 }
% 5.31/5.50 438 : P_line_connecting-{T}(E3,E0,E2) { 0, 11, 36 }
% 5.31/5.50 439 : pppp6-{T}(E3,E0,E0,E2) { 0, 11, 36 }
% 5.31/5.50 440 : pppp6-{T}(E3,E1,E0,E2) { 0, 11, 36 }
% 5.31/5.50 441 : pppp6-{T}(E3,E3,E0,E2) { 0, 11, 36 }
% 5.31/5.50 442 : pppp6-{T}(E3,E2,E0,E2) { 0, 9, 11, 36 }
% 5.31/5.50 443 : P_line_connecting-{T}(E3,E3,E2) { 0, 11, 37 }
% 5.31/5.50 444 : pppp6-{T}(E3,E0,E3,E2) { 0, 11, 37 }
% 5.31/5.50 445 : pppp6-{T}(E3,E1,E3,E2) { 0, 11, 37 }
% 5.31/5.50 446 : pppp6-{T}(E3,E3,E3,E2) { 0, 11, 37 }
% 5.31/5.50 447 : pppp6-{T}(E3,E2,E3,E2) { 0, 9, 11, 37 }
% 5.31/5.50 448 : P_intersection_point-{T}(E0,E3,E3) { 0, 11, 38 }
% 5.31/5.50 449 : P_parallel_through_point-{T}(E0,E3,E0) { 0, 11, 39 }
% 5.31/5.50 450 : P_intersection_point-{T}(E1,E3,E0) { 0, 11, 40 }
% 5.31/5.50 451 : P_parallel_through_point-{T}(E1,E3,E3) { 0, 11, 41 }
% 5.31/5.50 452 : P_line_connecting-{T}(E2,E3,E3) { 0, 9, 11, 42 }
% 5.31/5.50 453 : pppp6-{T}(E2,E0,E3,E3) { 0, 9, 11, 42 }
% 5.31/5.50 454 : pppp6-{T}(E2,E1,E3,E3) { 0, 9, 11, 42 }
% 5.31/5.50 455 : pppp6-{T}(E2,E2,E3,E3) { 0, 9, 11, 42 }
% 5.31/5.50 456 : pppp6-{T}(E2,E3,E3,E3) { 0, 9, 11, 42 }
% 5.31/5.50 457 : P_intersection_point-{T}(E3,E1,E1) { 0, 11, 43 }
% 5.31/5.50 458 : P_parallel_through_point-{T}(E3,E1,E3) { 0, 11, 44 }
% 5.31/5.50 459 : P_intersection_point-{T}(E3,E0,E3) { 0, 11, 45 }
% 5.31/5.50 460 : P_parallel_through_point-{T}(E3,E0,E3) { 0, 11, 46 }
% 5.31/5.50 461 : P_intersection_point-{T}(E3,E3,E0) { 0, 11, 47 }
% 5.31/5.50 462 : P_parallel_through_point-{T}(E3,E3,E3) { 0, 11, 48 }
% 5.31/5.50 463 : P_line_connecting-{T}(E3,E2,E3) { 0, 9, 11, 49 }
% 5.31/5.50 464 : pppp6-{T}(E3,E0,E2,E3) { 0, 9, 11, 49 }
% 5.31/5.50 465 : pppp6-{T}(E3,E1,E2,E3) { 0, 9, 11, 49 }
% 5.31/5.50 466 : pppp6-{T}(E3,E2,E2,E3) { 0, 9, 11, 49 }
% 5.31/5.50 467 : pppp6-{T}(E3,E3,E2,E3) { 0, 9, 11, 49 }
% 5.31/5.50 468 : P_intersection_point-{T}(E2,E3,E1) { 0, 9, 11, 50 }
% 5.31/5.50 469 : P_parallel_through_point-{T}(E2,E3,E2) { 0, 9, 11, 51 }
% 5.31/5.50 470 : P_intersection_point-{T}(E3,E2,E2) { 0, 9, 11, 52 }
% 5.31/5.50 471 : P_parallel_through_point-{T}(E3,E2,E3) { 0, 9, 11, 53 }
% 5.31/5.50
% 5.31/5.50
% 5.31/5.50 % SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.31/5.50
% 5.31/5.50 randbase = 1
%------------------------------------------------------------------------------