%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : LCL651+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:06:37 PM UTC 2026
% Result : CounterSatisfiable 9.25s 9.51s
% Output : Model 9.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL651+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.09/0.36 % Computer : n028.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 6 00:01:45 UTC 2026
% 0.09/0.36 % CPUTime :
% 9.25/9.51 GeoParameters:
% 9.25/9.51
% 9.25/9.51 tptp_input = 1
% 9.25/9.51 tptp_output = 0
% 9.25/9.51 nonempty = 1
% 9.25/9.51 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.25/9.51 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 9.25/9.51
% 9.25/9.51
% 9.25/9.51 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.25/9.51 % SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.25/9.51
% 9.25/9.51 Interpretation 156:
% 9.25/9.51 Guesses:
% 9.25/9.51 0 : guesser 1, 0, ( | 1, 0 ), 0, 9s old, 0 lemmas
% 9.25/9.51 1 : guesser 3, 1, ( | 1, 2, 0 ), 0, 9s old, 0 lemmas
% 9.25/9.51 2 : guesser 13, 11, ( | 0, 2, 1 ), 0, 9s old, 0 lemmas
% 9.25/9.51 3 : guesser 23, 21, ( | 0, 2, 1 ), 0, 9s old, 0 lemmas
% 9.25/9.51 4 : guesser 24, 22, ( | 0, 2, 1 ), 0, 9s old, 0 lemmas
% 9.25/9.51 5 : guesser 25, 23, ( | 1, 2, 0 ), 0, 9s old, 0 lemmas
% 9.25/9.51 6 : guesser 26, 24, ( | 1, 2, 0 ), 0, 9s old, 0 lemmas
% 9.25/9.51 7 : guesser 28, 26, ( | 1, 2, 0 ), 59, 6s old, 0 lemmas
% 9.25/9.51 8 : guesser 29, 27, ( | 0, 2, 1 ), 59, 6s old, 0 lemmas
% 9.25/9.51 9 : guesser 37, 35, ( | 0, 2, 1 ), 59, 6s old, 0 lemmas
% 9.25/9.51 10 : guesser 38, 36, ( | 1, 2, 0 ), 59, 6s old, 0 lemmas
% 9.25/9.51 11 : guesser 39, 37, ( | 1, 2, 0 ), 59, 6s old, 0 lemmas
% 9.25/9.52 12 : guesser 47, 45, ( | 1, 2, 0 ), 65, 6s old, 0 lemmas
% 9.25/9.52 13 : guesser 48, 46, ( 1 | 2, 0 ), 65, 6s old, 1 lemmas
% 9.25/9.52 14 : guesser 60, 57, ( 0 | 2, 3, 1 ), 99, 4s old, 1 lemmas
% 9.25/9.52 15 : guesser 62, 59, ( | 2, 1, 3, 0 ), 100, 4s old, 0 lemmas
% 9.25/9.52 16 : guesser 64, 61, ( | 2, 1, 3, 0 ), 101, 4s old, 0 lemmas
% 9.25/9.52 17 : guesser 65, 62, ( | 2, 1, 3, 0 ), 101, 4s old, 0 lemmas
% 9.25/9.52 18 : guesser 71, 68, ( 0 | 2, 3, 1 ), 102, 3s old, 1 lemmas
% 9.25/9.52 19 : guesser 72, 69, ( 1, 0 | 3, 2 ), 103, 3s old, 1 lemmas
% 9.25/9.52 20 : guesser 89, 85, ( | 0, 3, 2, 4, 1 ), 104, 3s old, 0 lemmas
% 9.25/9.52 21 : guesser 91, 87, ( | 0, 3, 2, 4, 1 ), 104, 3s old, 0 lemmas
% 9.25/9.52 22 : guesser 93, 89, ( 3, 2 | 1, 4, 0 ), 105, 3s old, 1 lemmas
% 9.25/9.52 23 : guesser 95, 91, ( | 0, 3, 2, 4, 1 ), 131, 1s old, 0 lemmas
% 9.25/9.52 24 : guesser 96, 92, ( 2 | 1, 0, 4, 3 ), 131, 1s old, 1 lemmas
% 9.25/9.52 25 : guesser 97, 93, ( 2 | 1, 0, 4, 3 ), 132, 1s old, 1 lemmas
% 9.25/9.52 26 : guesser 98, 94, ( | 0, 3, 2, 4, 1 ), 133, 1s old, 0 lemmas
% 9.25/9.52 27 : guesser 99, 95, ( 3, 2 | 1, 4, 0 ), 133, 1s old, 1 lemmas
% 9.25/9.52 28 : guesser 100, 96, ( | 2, 1, 0, 4, 3 ), 134, 1s old, 0 lemmas
% 9.25/9.52 29 : guesser 102, 98, ( 1, 0 | 3, 4, 2 ), 135, 1s old, 1 lemmas
% 9.25/9.52 30 : guesser 105, 101, ( 0 | 3, 2, 4, 1 ), 136, 1s old, 1 lemmas
% 9.25/9.52 31 : guesser 106, 102, ( | 2, 1, 0, 4, 3 ), 137, 1s old, 0 lemmas
% 9.25/9.52 32 : guesser 107, 103, ( 0 | 3, 2, 4, 1 ), 137, 1s old, 1 lemmas
% 9.25/9.52 33 : guesser 108, 104, ( 0 | 3, 2, 4, 1 ), 138, 1s old, 1 lemmas
% 9.25/9.52 34 : guesser 109, 105, ( 0 | 3, 2, 4, 1 ), 139, 1s old, 1 lemmas
% 9.25/9.52 35 : guesser 110, 106, ( | 1, 0, 3, 4, 2 ), 140, 1s old, 0 lemmas
% 9.25/9.52 36 : guesser 111, 107, ( | 3, 2, 1, 4, 0 ), 140, 1s old, 0 lemmas
% 9.25/9.52 37 : guesser 112, 108, ( | 0, 3, 2, 4, 1 ), 140, 1s old, 0 lemmas
% 9.25/9.52 38 : guesser 114, 110, ( 3, 2 | 1, 4, 0 ), 140, 1s old, 1 lemmas
% 9.25/9.52 39 : guesser 116, 112, ( 3, 2 | 1, 4, 0 ), 142, 1s old, 1 lemmas
% 9.25/9.52 40 : guesser 117, 113, ( | 0, 3, 2, 4, 1 ), 143, 1s old, 0 lemmas
% 9.25/9.52 41 : guesser 118, 114, ( | 0, 3, 2, 4, 1 ), 143, 1s old, 0 lemmas
% 9.25/9.52 42 : guesser 119, 115, ( 2 | 1, 0, 4, 3 ), 143, 1s old, 1 lemmas
% 9.25/9.52 43 : guesser 120, 116, ( | 1, 0, 3, 4, 2 ), 144, 1s old, 0 lemmas
% 9.25/9.52 44 : guesser 121, 117, ( 3, 2 | 1, 4, 0 ), 144, 1s old, 1 lemmas
% 9.25/9.52 45 : guesser 122, 118, ( | 3, 2, 1, 4, 0 ), 145, 1s old, 0 lemmas
% 9.25/9.52 46 : guesser 125, 121, ( 1, 0 | 3, 4, 2 ), 145, 1s old, 1 lemmas
% 9.25/9.52 47 : guesser 126, 122, ( | 3, 2, 1, 4, 0 ), 146, 1s old, 0 lemmas
% 9.25/9.52 48 : guesser 127, 123, ( | 3, 2, 1, 4, 0 ), 146, 1s old, 0 lemmas
% 9.25/9.52 49 : guesser 128, 124, ( | 2, 1, 0, 4, 3 ), 146, 1s old, 0 lemmas
% 9.25/9.52 50 : guesser 130, 126, ( 0 | 3, 2, 4, 1 ), 146, 1s old, 1 lemmas
% 9.25/9.52 51 : guesser 131, 127, ( 0 | 3, 2, 4, 1 ), 147, 1s old, 1 lemmas
% 9.25/9.52 52 : guesser 132, 128, ( | 1, 0, 3, 4, 2 ), 148, 1s old, 0 lemmas
% 9.25/9.52 53 : guesser 134, 130, ( | 0, 3, 2, 4, 1 ), 149, 0s old, 0 lemmas
% 9.25/9.52 54 : guesser 136, 132, ( 3, 2 | 1, 4, 0 ), 149, 0s old, 1 lemmas
% 9.25/9.52 55 : guesser 137, 133, ( | 1, 0, 3, 4, 2 ), 150, 0s old, 0 lemmas
% 9.25/9.52 56 : guesser 138, 134, ( | 1, 0, 3, 4, 2 ), 150, 0s old, 0 lemmas
% 9.25/9.52 57 : guesser 139, 135, ( | 1, 0, 3, 4, 2 ), 150, 0s old, 0 lemmas
% 9.25/9.52 58 : guesser 140, 136, ( | 0, 3, 2, 4, 1 ), 150, 0s old, 0 lemmas
% 9.25/9.52 59 : guesser 141, 137, ( 3, 2 | 1, 4, 0 ), 150, 0s old, 1 lemmas
% 9.25/9.52 60 : guesser 142, 138, ( 1, 0 | 3, 4, 2 ), 151, 0s old, 1 lemmas
% 9.25/9.52 61 : guesser 144, 140, ( 0 | 3, 2, 4, 1 ), 152, 0s old, 1 lemmas
% 9.25/9.52 62 : guesser 145, 141, ( | 3, 2, 1, 4, 0 ), 153, 0s old, 0 lemmas
% 9.25/9.52 63 : guesser 146, 142, ( 1, 0 | 3, 4, 2 ), 153, 0s old, 1 lemmas
% 9.25/9.52 64 : guesser 147, 143, ( | 2, 1, 0, 4, 3 ), 154, 0s old, 0 lemmas
% 9.25/9.52 65 : guesser 149, 145, ( | 3, 2, 1, 4, 0 ), 155, 0s old, 0 lemmas
% 9.25/9.52 66 : guesser 150, 146, ( 0 | 3, 2, 4, 1 ), 155, 0s old, 1 lemmas
% 9.25/9.52 67 : guesser 151, 147, ( | 3, 2, 1, 4, 0 ), 156, 0s old, 0 lemmas
% 9.25/9.52 68 : guesser 152, 148, ( | 2, 1, 0, 4, 3 ), 156, 0s old, 0 lemmas
% 9.25/9.52 69 : guesser 153, 149, ( | 2, 1, 0, 4, 3 ), 156, 0s old, 0 lemmas
% 9.25/9.52 70 : guesser 154, 150, ( | 3, 2, 1, 4, 0 ), 156, 0s old, 0 lemmas
% 9.25/9.52 71 : guesser 155, 151, ( | 0, 3, 2, 4, 1 ), 156, 0s old, 0 lemmas
% 9.25/9.52 72 : guesser 156, 152, ( | 2, 1, 0, 4, 3 ), 156, 0s old, 0 lemmas
% 9.25/9.52 73 : guesser 157, 153, ( | 2, 1, 0, 4, 3 ), 156, 0s old, 0 lemmas
% 9.25/9.52 74 : guesser 158, 154, ( | 2, 1, 0, 4, 3 ), 156, 0s old, 0 lemmas
% 9.25/9.52 75 : guesser 159, 155, ( | 1, 0, 3, 4, 2 ), 156, 0s old, 0 lemmas
% 9.25/9.52 76 : guesser 160, 156, ( | 3, 2, 1, 4, 0 ), 156, 0s old, 0 lemmas
% 9.25/9.52 77 : guesser 161, 157, ( | 1, 0, 3, 4, 2 ), 156, 0s old, 0 lemmas
% 9.25/9.52 78 : guesser 162, 158, ( | 2, 1, 0, 4, 3 ), 156, 0s old, 0 lemmas
% 9.25/9.52 79 : guesser 163, 159, ( | 2, 1, 0, 4, 3 ), 156, 0s old, 0 lemmas
% 9.25/9.52 80 : guesser 164, 160, ( | 1, 0, 3, 4, 2 ), 156, 0s old, 0 lemmas
% 9.25/9.52 81 : guesser 165, 161, ( | 2, 1, 0, 4, 3 ), 156, 0s old, 0 lemmas
% 9.25/9.52 82 : guesser 166, 162, ( | 0, 3, 2, 4, 1 ), 156, 0s old, 0 lemmas
% 9.25/9.52 83 : guesser 167, 163, ( | 1, 0, 3, 4, 2 ), 156, 0s old, 0 lemmas
% 9.25/9.52 84 : guesser 168, 164, ( | 2, 1, 0, 4, 3 ), 156, 0s old, 0 lemmas
% 9.25/9.52 85 : guesser 169, 165, ( | 3, 2, 1, 4, 0 ), 156, 0s old, 0 lemmas
% 9.25/9.52 86 : guesser 170, 166, ( | 0, 3, 2, 4, 1 ), 156, 0s old, 0 lemmas
% 9.25/9.52 87 : guesser 171, 167, ( | 2, 1, 0, 4, 3 ), 156, 0s old, 0 lemmas
% 9.25/9.52 88 : guesser 172, 168, ( | 0, 3, 2, 4, 1 ), 156, 0s old, 0 lemmas
% 9.25/9.52 89 : guesser 173, 169, ( | 0, 3, 2, 4, 1 ), 156, 0s old, 0 lemmas
% 9.25/9.52 90 : guesser 174, 170, ( | 3, 2, 1, 4, 0 ), 156, 0s old, 0 lemmas
% 9.25/9.52 91 : guesser 175, 171, ( | 3, 2, 1, 4, 0 ), 156, 0s old, 0 lemmas
% 9.25/9.52 92 : guesser 176, 172, ( | 0, 3, 2, 4, 1 ), 156, 0s old, 0 lemmas
% 9.25/9.52 93 : guesser 177, 173, ( | 1, 0, 3, 4, 2 ), 156, 0s old, 0 lemmas
% 9.25/9.52 94 : guesser 178, 174, ( | 3, 2, 1, 4, 0 ), 156, 0s old, 0 lemmas
% 9.25/9.52 95 : guesser 179, 175, ( | 0, 3, 2, 4, 1 ), 156, 0s old, 0 lemmas
% 9.25/9.52
% 9.25/9.52 Elements:
% 9.25/9.52 { E0, E1, E2, E3 }
% 9.25/9.52
% 9.25/9.52 Atoms:
% 9.25/9.52 0 : #-{T} E0 { }
% 9.25/9.52 1 : #-{T} E1 { 0 }
% 9.25/9.52 2 : pppp58-{T}(E1) { 0 }
% 9.25/9.52 3 : pppp57-{T}(E1,E1) { 0, 1 }
% 9.25/9.52 4 : r1-{T}(E1,E1) { 0, 1 }
% 9.25/9.52 5 : pppp40-{T}(E1) { 0, 1 }
% 9.25/9.52 6 : pppp39-{T}(E1) { 0, 1 }
% 9.25/9.52 7 : pppp38-{T}(E1) { 0, 1 }
% 9.25/9.52 8 : pppp37-{T}(E1) { 0, 1 }
% 9.25/9.52 9 : pppp36-{T}(E1) { 0, 1 }
% 9.25/9.52 10 : pppp35-{T}(E1) { 0, 1 }
% 9.25/9.52 11 : pppp34-{T}(E1) { 0, 1 }
% 9.25/9.52 12 : pppp33-{T}(E1) { 0, 1 }
% 9.25/9.52 13 : pppp17-{T}(E1,E0) { 0, 2 }
% 9.25/9.52 14 : r1-{T}(E1,E0) { 0, 2 }
% 9.25/9.52 15 : pppp40-{T}(E0) { 0, 2 }
% 9.25/9.52 16 : pppp39-{T}(E0) { 0, 1, 2 }
% 9.25/9.52 17 : pppp38-{T}(E0) { 0, 1, 2 }
% 9.25/9.52 18 : pppp37-{T}(E0) { 0, 1, 2 }
% 9.25/9.52 19 : pppp36-{T}(E0) { 0, 1, 2 }
% 9.25/9.52 20 : pppp35-{T}(E0) { 0, 1, 2 }
% 9.25/9.52 21 : pppp34-{T}(E0) { 0, 1, 2 }
% 9.25/9.52 22 : pppp33-{T}(E0) { 0, 1, 2 }
% 9.25/9.52 23 : pppp16-{T}(E1,E0) { 0, 3 }
% 9.25/9.52 24 : pppp56-{T}(E0,E1) { 0, 1, 4 }
% 9.25/9.52 25 : pppp18-{T}(E1,E1) { 0, 1, 5 }
% 9.25/9.52 26 : pppp20-{T}(E1,E1) { 0, 1, 6 }
% 9.25/9.52 27 : p16-{T}(E1) { 0, 1, 6 }
% 9.25/9.52 28 : pppp22-{T}(E1,E1) { 0, 1, 7 }
% 9.25/9.52 29 : pppp24-{T}(E0,E1) { 0, 1, 8 }
% 9.25/9.52 30 : p12-{T}(E0) { 0, 1, 2, 8 }
% 9.25/9.52 31 : p2-{T}(E0) { 0, 1, 2, 8 }
% 9.25/9.52 32 : p4-{T}(E0) { 0, 1, 2, 8 }
% 9.25/9.52 33 : p14-{T}(E0) { 0, 1, 2, 8 }
% 9.25/9.52 34 : p6-{T}(E0) { 0, 1, 2, 8 }
% 9.25/9.52 35 : p8-{T}(E0) { 0, 1, 2, 8 }
% 9.25/9.52 36 : p10-{T}(E0) { 0, 1, 2, 8 }
% 9.25/9.52 37 : pppp26-{T}(E0,E1) { 0, 1, 9 }
% 9.25/9.52 38 : pppp28-{T}(E1,E1) { 0, 1, 10 }
% 9.25/9.52 39 : pppp30-{T}(E1,E1) { 0, 1, 11 }
% 9.25/9.52 40 : p4-{T}(E1) { 0, 1, 11 }
% 9.25/9.52 41 : p6-{T}(E1) { 0, 1, 11 }
% 9.25/9.52 42 : p2-{T}(E1) { 0, 1, 11 }
% 9.25/9.52 43 : p8-{T}(E1) { 0, 1, 11 }
% 9.25/9.52 44 : p10-{T}(E1) { 0, 1, 11 }
% 9.25/9.52 45 : p12-{T}(E1) { 0, 1, 11 }
% 9.25/9.52 46 : p14-{T}(E1) { 0, 1, 11 }
% 9.25/9.52 47 : pppp32-{T}(E1,E1) { 0, 1, 12 }
% 9.25/9.52 48 : #-{T} E2 { 0, 1, 13 }
% 9.25/9.52 49 : pppp19-{T}(E1,E2) { 0, 1, 13 }
% 9.25/9.52 50 : r1-{T}(E1,E2) { 0, 1, 13 }
% 9.25/9.52 51 : pppp40-{T}(E2) { 0, 1, 13 }
% 9.25/9.52 52 : pppp39-{T}(E2) { 0, 1, 13 }
% 9.25/9.52 53 : pppp38-{T}(E2) { 0, 1, 13 }
% 9.25/9.52 54 : pppp37-{T}(E2) { 0, 1, 13 }
% 9.25/9.52 55 : pppp36-{T}(E2) { 0, 1, 13 }
% 9.25/9.52 56 : pppp35-{T}(E2) { 0, 1, 13 }
% 9.25/9.52 57 : pppp34-{T}(E2) { 0, 1, 13 }
% 9.25/9.52 58 : pppp33-{T}(E2) { 0, 1, 13 }
% 9.25/9.52 59 : p15-{T}(E2) { 0, 1, 13 }
% 9.25/9.52 60 : pppp21-{T}(E1,E2) { 0, 1, 14 }
% 9.25/9.52 61 : p13-{T}(E2) { 0, 1, 13, 14 }
% 9.25/9.52 62 : pppp23-{T}(E1,E2) { 0, 1, 15 }
% 9.25/9.52 63 : p11-{T}(E2) { 0, 1, 13, 15 }
% 9.25/9.52 64 : pppp25-{T}(E1,E2) { 0, 1, 16 }
% 9.25/9.52 65 : pppp27-{T}(E1,E2) { 0, 1, 17 }
% 9.25/9.52 66 : p9-{T}(E2) { 0, 1, 13, 17 }
% 9.25/9.52 67 : p1-{T}(E2) { 0, 1, 13, 17 }
% 9.25/9.52 68 : p3-{T}(E2) { 0, 1, 13, 17 }
% 9.25/9.52 69 : p5-{T}(E2) { 0, 1, 13, 17 }
% 9.25/9.52 70 : p7-{T}(E2) { 0, 1, 13, 17 }
% 9.25/9.52 71 : pppp29-{T}(E1,E2) { 0, 1, 18 }
% 9.25/9.52 72 : #-{T} E3 { 0, 1, 19 }
% 9.25/9.52 73 : pppp31-{T}(E1,E3) { 0, 1, 19 }
% 9.25/9.52 74 : r1-{T}(E1,E3) { 0, 1, 19 }
% 9.25/9.52 75 : pppp40-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 76 : pppp39-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 77 : pppp38-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 78 : pppp37-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 79 : pppp36-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 80 : pppp35-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 81 : pppp34-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 82 : pppp33-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 83 : p1-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 84 : p3-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 85 : p5-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 86 : p7-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 87 : p9-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 88 : p11-{T}(E3) { 0, 1, 19 }
% 9.25/9.52 89 : pppp18-{T}(E0,E0) { 0, 2, 20 }
% 9.25/9.52 90 : r1-{T}(E0,E0) { 0, 2, 20 }
% 9.25/9.52 91 : pppp20-{T}(E0,E0) { 0, 1, 2, 21 }
% 9.25/9.52 92 : p16-{T}(E0) { 0, 1, 2, 21 }
% 9.25/9.52 93 : pppp22-{T}(E1,E0) { 0, 1, 2, 22 }
% 9.25/9.52 94 : r1-{T}(E0,E1) { 0, 1, 2, 22 }
% 9.25/9.52 95 : pppp24-{T}(E0,E0) { 0, 1, 2, 23 }
% 9.25/9.52 96 : pppp26-{T}(E1,E0) { 0, 1, 2, 24 }
% 9.25/9.52 97 : pppp28-{T}(E1,E0) { 0, 1, 2, 25 }
% 9.25/9.52 98 : pppp30-{T}(E0,E0) { 0, 1, 2, 26 }
% 9.25/9.52 99 : pppp32-{T}(E1,E0) { 0, 1, 2, 27 }
% 9.25/9.52 100 : pppp19-{T}(E0,E2) { 0, 1, 2, 28 }
% 9.25/9.52 101 : r1-{T}(E0,E2) { 0, 1, 2, 28 }
% 9.25/9.52 102 : pppp21-{T}(E0,E3) { 0, 1, 2, 29 }
% 9.25/9.52 103 : r1-{T}(E0,E3) { 0, 1, 2, 29 }
% 9.25/9.52 104 : p13-{T}(E3) { 0, 1, 2, 19, 29 }
% 9.25/9.52 105 : pppp23-{T}(E0,E3) { 0, 1, 2, 30 }
% 9.25/9.52 106 : pppp25-{T}(E0,E2) { 0, 1, 2, 31 }
% 9.25/9.52 107 : pppp27-{T}(E0,E3) { 0, 1, 2, 32 }
% 9.25/9.52 108 : pppp29-{T}(E0,E3) { 0, 1, 2, 33 }
% 9.25/9.52 109 : pppp31-{T}(E0,E3) { 0, 1, 2, 34 }
% 9.25/9.52 110 : pppp15-{T}(E1,E0) { 0, 3, 35 }
% 9.25/9.52 111 : pppp55-{T}(E0,E3) { 0, 1, 4, 36 }
% 9.25/9.52 112 : pppp18-{T}(E0,E2) { 0, 1, 13, 37 }
% 9.25/9.52 113 : r1-{T}(E2,E0) { 0, 1, 13, 37 }
% 9.25/9.52 114 : pppp20-{T}(E1,E2) { 0, 1, 13, 38 }
% 9.25/9.52 115 : r1-{T}(E2,E1) { 0, 1, 13, 38 }
% 9.25/9.52 116 : pppp22-{T}(E1,E2) { 0, 1, 13, 39 }
% 9.25/9.52 117 : pppp24-{T}(E0,E2) { 0, 1, 13, 40 }
% 9.25/9.52 118 : pppp26-{T}(E0,E2) { 0, 1, 13, 41 }
% 9.25/9.52 119 : pppp28-{T}(E1,E2) { 0, 1, 13, 42 }
% 9.25/9.52 120 : pppp30-{T}(E1,E2) { 0, 1, 13, 43 }
% 9.25/9.52 121 : pppp32-{T}(E1,E2) { 0, 1, 13, 44 }
% 9.25/9.52 122 : pppp19-{T}(E2,E3) { 0, 1, 13, 45 }
% 9.25/9.52 123 : r1-{T}(E2,E3) { 0, 1, 13, 45 }
% 9.25/9.52 124 : p15-{T}(E3) { 0, 1, 13, 19, 45 }
% 9.25/9.52 125 : pppp21-{T}(E2,E3) { 0, 1, 13, 46 }
% 9.25/9.52 126 : pppp23-{T}(E2,E3) { 0, 1, 13, 47 }
% 9.25/9.52 127 : pppp25-{T}(E2,E3) { 0, 1, 13, 48 }
% 9.25/9.52 128 : pppp27-{T}(E2,E2) { 0, 1, 13, 49 }
% 9.25/9.52 129 : r1-{T}(E2,E2) { 0, 1, 13, 49 }
% 9.25/9.52 130 : pppp29-{T}(E2,E3) { 0, 1, 13, 50 }
% 9.25/9.52 131 : pppp31-{T}(E2,E3) { 0, 1, 13, 51 }
% 9.25/9.52 132 : pppp18-{T}(E1,E3) { 0, 1, 19, 52 }
% 9.25/9.52 133 : r1-{T}(E3,E1) { 0, 1, 19, 52 }
% 9.25/9.52 134 : pppp20-{T}(E0,E3) { 0, 1, 19, 53 }
% 9.25/9.52 135 : r1-{T}(E3,E0) { 0, 1, 19, 53 }
% 9.25/9.52 136 : pppp22-{T}(E1,E3) { 0, 1, 19, 54 }
% 9.25/9.52 137 : pppp24-{T}(E1,E3) { 0, 1, 19, 55 }
% 9.25/9.52 138 : pppp26-{T}(E1,E3) { 0, 1, 19, 56 }
% 9.25/9.52 139 : pppp28-{T}(E1,E3) { 0, 1, 19, 57 }
% 9.25/9.52 140 : pppp30-{T}(E0,E3) { 0, 1, 19, 58 }
% 9.25/9.52 141 : pppp32-{T}(E1,E3) { 0, 1, 19, 59 }
% 9.25/9.52 142 : pppp19-{T}(E3,E3) { 0, 1, 19, 60 }
% 9.25/9.52 143 : r1-{T}(E3,E3) { 0, 1, 19, 60 }
% 9.25/9.52 144 : pppp21-{T}(E3,E3) { 0, 1, 19, 61 }
% 9.25/9.52 145 : pppp23-{T}(E3,E3) { 0, 1, 19, 62 }
% 9.25/9.52 146 : pppp25-{T}(E3,E3) { 0, 1, 19, 63 }
% 9.25/9.52 147 : pppp27-{T}(E3,E2) { 0, 1, 19, 64 }
% 9.25/9.52 148 : r1-{T}(E3,E2) { 0, 1, 19, 64 }
% 9.25/9.52 149 : pppp29-{T}(E3,E3) { 0, 1, 19, 65 }
% 9.25/9.52 150 : pppp31-{T}(E3,E3) { 0, 1, 19, 66 }
% 9.25/9.52 151 : pppp14-{T}(E1,E3) { 0, 3, 35, 67 }
% 9.25/9.52 152 : pppp54-{T}(E2,E3) { 0, 1, 4, 36, 68 }
% 9.25/9.52 153 : pppp13-{T}(E2,E3) { 0, 3, 35, 67, 69 }
% 9.25/9.52 154 : pppp53-{T}(E2,E3) { 0, 1, 4, 36, 68, 70 }
% 9.25/9.52 155 : pppp12-{T}(E2,E0) { 0, 3, 35, 67, 69, 71 }
% 9.25/9.52 156 : pppp52-{T}(E2,E3) { 0, 1, 4, 36, 68, 70, 72 }
% 9.25/9.52 157 : pppp11-{T}(E2,E0) { 0, 3, 35, 67, 69, 71, 73 }
% 9.25/9.52 158 : pppp51-{T}(E2,E2) { 0, 1, 4, 36, 68, 70, 72, 74 }
% 9.25/9.52 159 : pppp10-{T}(E2,E1) { 0, 3, 35, 67, 69, 71, 73, 75 }
% 9.25/9.52 160 : pppp50-{T}(E3,E2) { 0, 1, 4, 36, 68, 70, 72, 74, 76 }
% 9.25/9.52 161 : pppp9-{T}(E1,E1) { 0, 3, 35, 67, 69, 71, 73, 75, 77 }
% 9.25/9.52 162 : pppp49-{T}(E3,E2) { 0, 1, 4, 36, 68, 70, 72, 74, 76, 78 }
% 9.25/9.52 163 : pppp8-{T}(E1,E2) { 0, 3, 35, 67, 69, 71, 73, 75, 77, 79 }
% 9.25/9.52 164 : pppp48-{T}(E1,E2) { 0, 1, 4, 36, 68, 70, 72, 74, 76, 78, 80 }
% 9.25/9.52 165 : pppp7-{T}(E2,E2) { 0, 3, 35, 67, 69, 71, 73, 75, 77, 79, 81 }
% 9.25/9.52 166 : pppp47-{T}(E1,E0) { 0, 1, 4, 36, 68, 70, 72, 74, 76, 78, 80, 82 }
% 9.25/9.52 167 : pppp6-{T}(E2,E1) { 0, 3, 35, 67, 69, 71, 73, 75, 77, 79, 81, 83 }
% 9.25/9.52 168 : pppp46-{T}(E2,E0) { 0, 1, 4, 36, 68, 70, 72, 74, 76, 78, 80, 82, 84 }
% 9.25/9.52 169 : pppp5-{T}(E3,E1) { 0, 3, 35, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85 }
% 9.25/9.52 170 : pppp45-{T}(E2,E0) { 0, 1, 4, 36, 68, 70, 72, 74, 76, 78, 80, 82, 84, 86 }
% 9.25/9.52 171 : pppp4-{T}(E3,E2) { 0, 3, 35, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85, 87 }
% 9.25/9.52 172 : pppp44-{T}(E0,E0) { 0, 1, 4, 36, 68, 70, 72, 74, 76, 78, 80, 82, 84, 86, 88 }
% 9.25/9.52 173 : pppp3-{T}(E0,E2) { 0, 3, 35, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85, 87, 89 }
% 9.25/9.52 174 : pppp43-{T}(E0,E3) { 0, 1, 4, 36, 68, 70, 72, 74, 76, 78, 80, 82, 84, 86, 88, 90 }
% 9.25/9.52 175 : pppp2-{T}(E0,E3) { 0, 3, 35, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85, 87, 89, 91 }
% 9.25/9.52 176 : pppp42-{T}(E0,E3) { 0, 1, 4, 36, 68, 70, 72, 74, 76, 78, 80, 82, 84, 86, 88, 90, 92 }
% 9.25/9.52 177 : pppp1-{T}(E1,E3) { 0, 3, 35, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85, 87, 89, 91, 93 }
% 9.25/9.52 178 : pppp41-{T}(E0,E3) { 0, 1, 4, 36, 68, 70, 72, 74, 76, 78, 80, 82, 84, 86, 88, 90, 92, 94 }
% 9.25/9.52 179 : pppp0-{T}(E1,E0) { 0, 3, 35, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85, 87, 89, 91, 93, 95 }
% 9.25/9.52
% 9.25/9.52
% 9.25/9.52 % SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.25/9.52
% 9.25/9.52 randbase = 1
%------------------------------------------------------------------------------