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