%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN720-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n005.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 : 0s % DateTime : Thu Jul 21 03:52:26 EDT 2022 % Result : Satisfiable 0.18s 0.42s % Output : Model 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SYN720-1 : TPTP v8.1.0. Released v2.5.0. % 0.11/0.12 % Command : darwin -pl 0 -pmc true -to %d %s % 0.12/0.33 % Computer : n005.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 % DateTime : Tue Jul 12 07:03:06 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.34 Defaulting to tptp format. % 0.18/0.42 SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.42 % 0.18/0.42 MODEL (CONTEXT): % 0.18/0.42 SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.42 -__-v__(=0) % 0.18/0.42 +__con100 % 0.18/0.42 +__con101 % 0.18/0.42 +__con102 % 0.18/0.42 +__con103 % 0.18/0.42 +__con104 % 0.18/0.42 +__con105 % 0.18/0.42 +__con106 % 0.18/0.42 +__con107 % 0.18/0.42 +__con108 % 0.18/0.42 +__con109 % 0.18/0.42 +__con110 % 0.18/0.42 +__con111 % 0.18/0.42 +__con112 % 0.18/0.42 +__con113 % 0.18/0.42 +__con114 % 0.18/0.42 +__con115 % 0.18/0.42 +__con116 % 0.18/0.42 +__con117 % 0.18/0.42 +__con118 % 0.18/0.42 +__con119 % 0.18/0.42 +__con120 % 0.18/0.42 +__con121 % 0.18/0.42 +__con122 % 0.18/0.42 +__con123 % 0.18/0.42 +__con124 % 0.18/0.42 +__con125 % 0.18/0.42 +__con126 % 0.18/0.42 +__con127 % 0.18/0.42 +__con128 % 0.18/0.42 +__con129 % 0.18/0.42 +__con130 % 0.18/0.42 +__con131 % 0.18/0.42 +__con132 % 0.18/0.42 +__con133 % 0.18/0.42 +__con134 % 0.18/0.42 +__con135 % 0.18/0.42 +__con136 % 0.18/0.42 +__con137 % 0.18/0.42 +__con138 % 0.18/0.42 +__con139 % 0.18/0.42 +__con140 % 0.18/0.42 +__con141 % 0.18/0.42 +__con142 % 0.18/0.42 +__con143 % 0.18/0.42 +__con144 % 0.18/0.42 +__con145 % 0.18/0.42 +__con146 % 0.18/0.42 +__con147 % 0.18/0.42 +__con148 % 0.18/0.42 +__con149 % 0.18/0.42 +__con150 % 0.18/0.42 +__con151 % 0.18/0.42 +__con152 % 0.18/0.42 +__con153 % 0.18/0.42 +__con154 % 0.18/0.42 +__con155 % 0.18/0.42 +__con156 % 0.18/0.42 +__con157 % 0.18/0.42 +__con158 % 0.18/0.42 +__con159 % 0.18/0.42 +__con160 % 0.18/0.42 +__con161 % 0.18/0.42 +__con162 % 0.18/0.42 +__con163 % 0.18/0.42 +__con164 % 0.18/0.42 +__con165 % 0.18/0.42 +__con166 % 0.18/0.42 +__con65 % 0.18/0.42 +__con66 % 0.18/0.42 +__con67 % 0.18/0.42 +__con68 % 0.18/0.42 +__con69 % 0.18/0.42 +__con70 % 0.18/0.42 +__con71 % 0.18/0.42 +__con72 % 0.18/0.42 +__con75 % 0.18/0.42 +__con76 % 0.18/0.42 +__con77 % 0.18/0.42 +__con78 % 0.18/0.42 +__con79 % 0.18/0.42 +__con80 % 0.18/0.42 +__con81 % 0.18/0.42 +__con82 % 0.18/0.42 +__con83 % 0.18/0.42 +__con84 % 0.18/0.42 +__con85 % 0.18/0.42 +__con86 % 0.18/0.42 +__con87 % 0.18/0.42 +__con88 % 0.18/0.42 +__con89 % 0.18/0.42 +__con90 % 0.18/0.42 +__con91 % 0.18/0.42 +__con92 % 0.18/0.42 +__con93 % 0.18/0.42 +__con94 % 0.18/0.42 +__con95 % 0.18/0.42 +__con96 % 0.18/0.42 +__con97 % 0.18/0.42 +__con98 % 0.18/0.42 +__con99 % 0.18/0.42 +k0(e) % 0.18/0.42 +k0(b) % 0.18/0.42 -k0(a) % 0.18/0.42 +k1(d) % 0.18/0.42 +k1(e) % 0.18/0.42 +k1(a) % 0.18/0.42 +k1(b) % 0.18/0.42 +k1(c) % 0.18/0.42 +k2(_0, _0) % 0.18/0.42 +k2(_0, d) % 0.18/0.42 +k2(e, a) % 0.18/0.42 +k2(e, b) % 0.18/0.42 +k2(e, c) % 0.18/0.42 +k2(a, e) % 0.18/0.42 +k2(a, b) % 0.18/0.42 +k2(b, e) % 0.18/0.42 +k2(b, a) % 0.18/0.42 +k2(b, c) % 0.18/0.42 +k2(c, e) % 0.18/0.42 +k2(c, a) % 0.18/0.42 +k2(c, b) % 0.18/0.42 +k3(_0, _0, _0) % 0.18/0.42 +k3(_0, _0, d) % 0.18/0.42 +k3(_0, _0, e) % 0.18/0.42 +k3(_0, _0, b) % 0.18/0.42 +k3(_0, _0, c) % 0.18/0.42 +k3(_0, d, _0) % 0.18/0.42 +k3(d, d, _0) % 0.18/0.42 +k3(d, e, d) % 0.18/0.42 +k3(d, a, d) % 0.18/0.42 +k3(d, b, d) % 0.18/0.42 +k3(d, c, d) % 0.18/0.42 +k3(e, _0, e) % 0.18/0.42 +k3(e, e, a) % 0.18/0.42 +k3(a, _0, a) % 0.18/0.42 +k3(a, a, _0) % 0.18/0.42 +k3(b, _0, b) % 0.18/0.42 +k3(b, b, a) % 0.18/0.42 +k3(c, _0, c) % 0.18/0.42 +k3(c, e, c) % 0.18/0.42 +k3(c, b, c) % 0.18/0.42 -k3(c, e, b) % 0.18/0.42 +k4(e) % 0.18/0.42 +k4(c) % 0.18/0.42 +k5(_0) % 0.18/0.42 +k5(b) % 0.18/0.42 +l0(a) % 0.18/0.42 +l0(c) % 0.18/0.42 -l0(b) % 0.18/0.42 +l1(d, _0) % 0.18/0.42 +l1(d, d) % 0.18/0.42 +l1(e, e) % 0.18/0.42 +l1(a, a) % 0.18/0.42 +l1(b, e) % 0.18/0.42 +l1(b, b) % 0.18/0.42 +l1(c, c) % 0.18/0.42 +l2(_0, _0) % 0.18/0.42 +l2(_0, e) % 0.18/0.42 +l2(_0, b) % 0.18/0.42 +l2(d, d) % 0.18/0.42 +l2(e, e) % 0.18/0.42 +l2(a, a) % 0.18/0.42 +l2(b, e) % 0.18/0.42 +l2(b, b) % 0.18/0.42 +l2(c, c) % 0.18/0.42 +l3(_0, _0) % 0.18/0.42 +l3(d, c) % 0.18/0.42 +l3(e, d) % 0.18/0.42 +l3(e, a) % 0.18/0.42 +l3(e, b) % 0.18/0.42 +l3(e, c) % 0.18/0.42 +l3(b, e) % 0.18/0.42 +l3(b, a) % 0.18/0.42 +l3(b, c) % 0.18/0.42 +l4(_0) % 0.18/0.42 +l5(d) % 0.18/0.42 +l5(e) % 0.18/0.42 +l5(a) % 0.18/0.42 +l5(b) % 0.18/0.42 +l5(c) % 0.18/0.42 +m0(_0, d, _1) % 0.18/0.42 +m0(d, e, c) % 0.18/0.42 +m0(e, b, c) % 0.18/0.42 +m0(a, _0, a) % 0.18/0.42 +m0(a, e, e) % 0.18/0.42 +m0(b, a, a) % 0.18/0.42 +m0(b, b, e) % 0.18/0.42 +m0(c, b, a) % 0.18/0.42 -m0(_0, c, b) % 0.18/0.42 -m0(a, e, c) % 0.18/0.42 -m0(b, c, e) % 0.18/0.42 +m1(_0, _0, _0) % 0.18/0.42 +m1(_0, d, _0) % 0.18/0.42 +m1(_0, d, d) % 0.18/0.42 +m1(d, e, e) % 0.18/0.42 +m1(d, a, a) % 0.18/0.42 +m1(d, a, b) % 0.18/0.42 +m1(d, a, c) % 0.18/0.42 +m1(d, b, b) % 0.18/0.42 +m1(d, c, c) % 0.18/0.42 +m1(e, _0, e) % 0.18/0.42 +m1(e, e, e) % 0.18/0.42 +m1(e, a, a) % 0.18/0.42 +m1(e, b, b) % 0.18/0.42 +m1(a, e, a) % 0.18/0.42 +m1(a, a, a) % 0.18/0.42 +m1(a, a, b) % 0.18/0.42 +m1(a, b, a) % 0.18/0.42 +m1(a, b, b) % 0.18/0.42 +m1(b, _0, b) % 0.18/0.42 +m1(b, d, d) % 0.18/0.42 +m1(b, e, e) % 0.18/0.42 +m1(b, a, e) % 0.18/0.42 +m1(b, a, a) % 0.18/0.42 +m1(b, b, e) % 0.18/0.42 +m1(b, c, c) % 0.18/0.42 +m1(c, e, c) % 0.18/0.42 +m1(c, a, a) % 0.18/0.42 +m1(c, b, c) % 0.18/0.42 +m1(c, c, c) % 0.18/0.42 -m1(c, d, a) % 0.18/0.42 +m2(d) % 0.18/0.42 +m2(b) % 0.18/0.42 +m3(_0, _0, _0) % 0.18/0.42 +m3(_0, d, d) % 0.18/0.42 +m3(_0, e, e) % 0.18/0.42 +m3(_0, b, b) % 0.18/0.42 +m3(d, _0, d) % 0.18/0.42 +m3(d, d, a) % 0.18/0.42 +m3(d, d, c) % 0.18/0.42 +m3(d, e, d) % 0.18/0.42 +m3(d, a, d) % 0.18/0.42 +m3(e, _0, e) % 0.18/0.42 +m3(e, e, a) % 0.18/0.42 +m3(e, e, c) % 0.18/0.42 +m3(a, _0, a) % 0.18/0.42 +m3(a, d, a) % 0.18/0.42 +m3(a, e, a) % 0.18/0.42 +m3(a, a, c) % 0.18/0.42 +m3(a, b, a) % 0.18/0.42 +m3(a, c, a) % 0.18/0.42 +m3(b, _0, b) % 0.18/0.42 +m3(b, b, a) % 0.18/0.42 +m3(b, b, c) % 0.18/0.42 +m3(c, d, c) % 0.18/0.42 +m3(c, e, c) % 0.18/0.42 +m3(c, a, c) % 0.18/0.42 +m3(c, b, d) % 0.18/0.42 +m3(c, b, c) % 0.18/0.42 +m3(c, c, a) % 0.18/0.42 +m4(_0, _1) % 0.18/0.42 +m4(_0, d) % 0.18/0.42 +m4(_0, e) % 0.18/0.42 +m4(_0, a) % 0.18/0.42 +m4(_0, b) % 0.18/0.42 +m4(_0, c) % 0.18/0.42 +m5(_0, _1) % 0.18/0.42 +n0(d, e) % 0.18/0.42 +n0(d, b) % 0.18/0.42 +n0(d, c) % 0.18/0.42 +n0(e, e) % 0.18/0.42 +n0(e, b) % 0.18/0.42 +n0(a, b) % 0.18/0.42 +n0(b, a) % 0.18/0.42 +n0(c, d) % 0.18/0.42 +n1(_0, _0, _1) % 0.18/0.42 +n1(d, d, d) % 0.18/0.42 +n1(d, e, e) % 0.18/0.42 +n1(d, c, d) % 0.18/0.42 +n1(e, a, e) % 0.18/0.42 +n1(e, c, e) % 0.18/0.42 +n1(a, _0, _0) % 0.18/0.42 +n1(a, _0, a) % 0.18/0.42 +n1(b, e, e) % 0.18/0.42 +n1(b, a, b) % 0.18/0.42 +n1(b, c, b) % 0.18/0.42 +n1(c, _0, _0) % 0.18/0.42 +n1(c, _0, c) % 0.18/0.42 +n1(c, c, c) % 0.18/0.42 +n2(_0) % 0.18/0.42 +n3(_0) % 0.18/0.42 +n4(_0, _0) % 0.18/0.42 +n4(_0, e) % 0.18/0.42 +n4(_0, a) % 0.18/0.42 +n4(_0, b) % 0.18/0.42 +n4(d, _0) % 0.18/0.42 +n4(d, d) % 0.18/0.42 +n4(e, _0) % 0.18/0.42 +n4(b, c) % 0.18/0.42 +n5(_0, _0) % 0.18/0.42 +n5(_0, _1) % 0.18/0.42 +n5(d, _0) % 0.18/0.42 +p0(b, _0) % 0.18/0.42 +p0(c, b) % 0.18/0.42 -p0(d, d) % 0.18/0.42 -p0(d, b) % 0.18/0.42 -p0(a, b) % 0.18/0.42 -p0(a, c) % 0.18/0.42 +p1(_0, _0, _0) % 0.18/0.42 +p1(_0, _0, b) % 0.18/0.42 +p1(_0, _1, a) % 0.18/0.42 +p1(_0, d, _0) % 0.18/0.42 +p1(d, _0, _1) % 0.18/0.42 +p1(e, _0, d) % 0.18/0.42 +p1(e, e, e) % 0.18/0.42 +p1(e, b, e) % 0.18/0.42 +p1(e, b, b) % 0.18/0.42 +p1(e, c, e) % 0.18/0.42 +p1(a, _0, a) % 0.18/0.42 +p1(a, _0, b) % 0.18/0.42 +p1(a, a, a) % 0.18/0.42 +p1(a, b, a) % 0.18/0.42 +p1(b, _0, a) % 0.18/0.42 +p1(b, _0, b) % 0.18/0.42 +p1(b, _0, c) % 0.18/0.42 +p1(b, b, e) % 0.18/0.42 +p1(c, b, c) % 0.18/0.42 +p1(c, c, e) % 0.18/0.42 +p2(_0, _0, _0) % 0.18/0.42 +p2(_0, e, _0) % 0.18/0.42 +p2(_0, e, e) % 0.18/0.42 +p2(_0, a, _0) % 0.18/0.42 +p2(_0, a, a) % 0.18/0.42 +p2(_0, b, _0) % 0.18/0.42 +p2(_0, b, b) % 0.18/0.42 +p2(d, _0, _0) % 0.18/0.42 +p2(d, _0, d) % 0.18/0.42 +p2(e, d, _0) % 0.18/0.42 +p2(e, e, d) % 0.18/0.42 +p2(e, e, b) % 0.18/0.42 +p2(e, e, c) % 0.18/0.42 +p2(e, c, e) % 0.18/0.42 +p2(e, c, c) % 0.18/0.42 +p2(b, c, a) % 0.18/0.42 +p2(b, c, b) % 0.18/0.42 +p2(b, c, c) % 0.18/0.42 -p2(d, b, c) % 0.18/0.42 +p3(_0, _0, _0) % 0.18/0.42 +p3(_0, e, e) % 0.18/0.42 +p3(_0, a, a) % 0.18/0.42 +p3(_0, b, b) % 0.18/0.42 +p3(d, _0, _0) % 0.18/0.42 +p3(d, _0, d) % 0.18/0.42 +p3(d, e, a) % 0.18/0.42 +p3(d, e, b) % 0.18/0.42 +p3(d, e, c) % 0.18/0.42 +p3(d, a, e) % 0.18/0.42 +p3(d, a, b) % 0.18/0.42 +p3(d, b, e) % 0.18/0.42 +p3(d, b, a) % 0.18/0.42 +p3(d, b, c) % 0.18/0.42 +p3(d, c, e) % 0.18/0.42 +p3(d, c, a) % 0.18/0.42 +p3(d, c, b) % 0.18/0.42 +p3(e, _0, _0) % 0.18/0.42 +p3(e, _0, d) % 0.18/0.42 +p3(e, e, a) % 0.18/0.42 +p3(e, e, b) % 0.18/0.42 +p3(e, e, c) % 0.18/0.42 +p3(e, a, e) % 0.18/0.42 +p3(e, a, b) % 0.18/0.42 +p3(e, b, e) % 0.18/0.42 +p3(e, b, a) % 0.18/0.42 +p3(e, b, c) % 0.18/0.42 +p3(e, c, e) % 0.18/0.42 +p3(e, c, a) % 0.18/0.42 +p3(e, c, b) % 0.18/0.42 +p3(a, a, _0) % 0.18/0.42 +p3(b, c, b) % 0.18/0.42 +p3(b, c, c) % 0.18/0.42 +p3(c, c, _0) % 0.18/0.42 +p3(c, c, d) % 0.18/0.42 +p3(c, c, e) % 0.18/0.42 +p3(c, c, b) % 0.18/0.42 +p4(_0, _0, _0) % 0.18/0.42 +p4(_0, d, _0) % 0.18/0.42 +p4(_0, e, _0) % 0.18/0.42 +p4(_0, b, _0) % 0.18/0.42 +p4(_0, c, _0) % 0.18/0.42 +p4(d, _0, d) % 0.18/0.42 +p4(d, e, e) % 0.18/0.42 +p4(d, a, a) % 0.18/0.42 +p4(d, b, b) % 0.18/0.42 +p4(d, c, c) % 0.18/0.42 +p4(e, e, _0) % 0.18/0.42 +p4(e, a, e) % 0.18/0.42 +p4(e, a, a) % 0.18/0.42 +p4(a, _0, a) % 0.18/0.42 +p4(a, c, c) % 0.18/0.42 +p4(b, d, d) % 0.18/0.42 +p4(b, e, e) % 0.18/0.42 +p4(b, a, a) % 0.18/0.42 +p4(b, a, b) % 0.18/0.42 +p4(b, b, _0) % 0.18/0.42 +p4(b, c, c) % 0.18/0.42 +p4(c, e, e) % 0.18/0.42 +p4(c, b, b) % 0.18/0.42 +p4(c, c, a) % 0.18/0.42 +p5(_0, _0, d) % 0.18/0.42 +p5(_0, _0, e) % 0.18/0.42 +p5(_0, _0, a) % 0.18/0.42 +p5(_0, _0, b) % 0.18/0.42 +p5(_0, _0, c) % 0.18/0.42 +p5(_0, _1, _0) % 0.18/0.42 +p5(_0, _1, _1) % 0.18/0.42 +p5(d, d, e) % 0.18/0.42 +p5(d, d, a) % 0.18/0.42 +p5(d, d, b) % 0.18/0.42 +p5(d, d, c) % 0.18/0.42 +p5(e, e, d) % 0.18/0.42 +p5(e, e, a) % 0.18/0.42 +p5(e, e, b) % 0.18/0.42 +p5(e, e, c) % 0.18/0.42 +p5(a, a, d) % 0.18/0.42 +p5(a, a, e) % 0.18/0.42 +p5(a, a, b) % 0.18/0.42 +p5(a, a, c) % 0.18/0.42 +p5(b, _0, b) % 0.18/0.42 +p5(b, b, d) % 0.18/0.42 +p5(b, b, e) % 0.18/0.42 +p5(b, b, a) % 0.18/0.42 +p5(b, b, c) % 0.18/0.42 +p5(c, c, d) % 0.18/0.42 +p5(c, c, e) % 0.18/0.42 +p5(c, c, a) % 0.18/0.42 +p5(c, c, b) % 0.18/0.42 +q0(_0, d) % 0.18/0.42 +q0(d, b) % 0.18/0.42 +q0(d, c) % 0.18/0.42 +q0(a, b) % 0.18/0.42 +q0(b, e) % 0.18/0.42 +q0(b, b) % 0.18/0.42 -q0(e, c) % 0.18/0.42 +q1(_0, _0, _0) % 0.18/0.42 +q1(_0, _0, d) % 0.18/0.42 +q1(_0, d, _0) % 0.18/0.42 +q1(_0, e, _0) % 0.18/0.42 +q1(_0, a, _0) % 0.18/0.42 +q1(_0, b, _0) % 0.18/0.42 +q1(_0, b, b) % 0.18/0.42 +q1(_0, c, _0) % 0.18/0.42 +q1(d, d, _0) % 0.18/0.42 +q1(d, d, d) % 0.18/0.42 +q1(d, d, b) % 0.18/0.42 +q1(e, _0, _0) % 0.18/0.42 +q1(e, e, a) % 0.18/0.42 +q1(e, e, b) % 0.18/0.42 +q1(a, d, d) % 0.18/0.42 +q1(a, e, e) % 0.18/0.42 +q1(a, a, b) % 0.18/0.42 +q1(b, b, d) % 0.18/0.42 +q1(b, b, e) % 0.18/0.42 +q1(b, b, a) % 0.18/0.42 +q1(b, b, b) % 0.18/0.42 +q1(b, b, c) % 0.18/0.42 +q1(b, c, c) % 0.18/0.42 +q1(c, d, d) % 0.18/0.42 +q1(c, e, e) % 0.18/0.42 +q1(c, a, a) % 0.18/0.42 +q1(c, c, d) % 0.18/0.42 +q1(c, c, a) % 0.18/0.42 -q1(c, a, d) % 0.18/0.42 +q2(_0, _0, _0) % 0.18/0.42 +q2(_0, _0, d) % 0.18/0.42 +q2(_0, e, _0) % 0.18/0.42 +q2(_0, e, e) % 0.18/0.42 +q2(_0, b, _0) % 0.18/0.42 +q2(_0, b, b) % 0.18/0.42 +q2(d, a, d) % 0.18/0.42 +q2(d, c, d) % 0.18/0.42 +q2(e, d, e) % 0.18/0.42 +q2(e, e, b) % 0.18/0.42 +q2(e, a, e) % 0.18/0.42 +q2(e, c, d) % 0.18/0.42 +q2(e, c, e) % 0.18/0.42 +q2(e, c, a) % 0.18/0.42 +q2(e, c, b) % 0.18/0.42 +q2(e, c, c) % 0.18/0.42 +q2(a, c, a) % 0.18/0.42 +q2(b, a, b) % 0.18/0.42 +q2(b, c, d) % 0.18/0.42 +q2(b, c, e) % 0.18/0.42 +q2(b, c, a) % 0.18/0.42 +q2(b, c, b) % 0.18/0.42 +q2(b, c, c) % 0.18/0.42 +q3(d, d) % 0.18/0.42 +q3(d, e) % 0.18/0.42 +q3(d, b) % 0.18/0.42 +q3(d, c) % 0.18/0.42 +q3(e, d) % 0.18/0.42 +q3(e, e) % 0.18/0.42 +q3(e, b) % 0.18/0.42 +q3(a, a) % 0.18/0.42 +q3(a, b) % 0.18/0.42 +q3(b, d) % 0.18/0.42 +q3(b, e) % 0.18/0.42 +q3(b, a) % 0.18/0.42 +q3(b, b) % 0.18/0.42 +q3(c, d) % 0.18/0.42 +q3(c, c) % 0.18/0.42 +q4(_0, _0) % 0.18/0.42 +q4(_0, e) % 0.18/0.42 +q4(_0, b) % 0.18/0.42 +q4(d, _0) % 0.18/0.42 +q4(d, c) % 0.18/0.42 +q4(e, d) % 0.18/0.42 +q4(e, a) % 0.18/0.42 +q4(e, c) % 0.18/0.42 +q4(a, c) % 0.18/0.42 +q4(b, a) % 0.18/0.42 +q4(b, c) % 0.18/0.42 +q5(_0, _1) % 0.18/0.42 +r0(e) % 0.18/0.42 +r0(b) % 0.18/0.42 -r0(d) % 0.18/0.42 -r0(a) % 0.18/0.42 -r0(c) % 0.18/0.42 +r1(_0) % 0.18/0.42 +r2(a) % 0.18/0.42 +r2(c) % 0.18/0.42 +r3(_0, _0, _0) % 0.18/0.42 +r3(_0, e, _0) % 0.18/0.42 +r3(_0, a, _0) % 0.18/0.42 +r3(_0, b, _0) % 0.18/0.42 +r3(d, _0, d) % 0.18/0.42 +r3(d, d, b) % 0.18/0.42 +r3(d, e, c) % 0.18/0.42 +r3(d, b, c) % 0.18/0.42 +r3(d, c, c) % 0.18/0.42 +r3(e, _0, e) % 0.18/0.42 +r3(e, d, d) % 0.18/0.42 +r3(e, e, d) % 0.18/0.42 +r3(e, e, b) % 0.18/0.42 +r3(e, e, c) % 0.18/0.42 +r3(e, a, a) % 0.18/0.42 +r3(e, b, b) % 0.18/0.42 +r3(e, b, c) % 0.18/0.42 +r3(e, c, c) % 0.18/0.42 +r3(a, e, c) % 0.18/0.42 +r3(a, a, d) % 0.18/0.42 +r3(a, a, e) % 0.18/0.42 +r3(a, a, b) % 0.18/0.42 +r3(a, b, c) % 0.18/0.42 +r3(a, c, a) % 0.18/0.42 +r3(a, c, c) % 0.18/0.42 +r3(b, d, d) % 0.18/0.42 +r3(b, e, e) % 0.18/0.42 +r3(b, e, c) % 0.18/0.42 +r3(b, a, a) % 0.18/0.42 +r3(b, b, d) % 0.18/0.42 +r3(b, b, c) % 0.18/0.42 +r3(b, c, b) % 0.18/0.42 +r3(b, c, c) % 0.18/0.42 +r3(c, d, d) % 0.18/0.42 +r3(c, e, e) % 0.18/0.42 +r3(c, e, a) % 0.18/0.42 +r3(c, a, a) % 0.18/0.42 +r3(c, b, a) % 0.18/0.42 +r3(c, b, b) % 0.18/0.42 +r3(c, c, d) % 0.18/0.42 +r3(c, c, a) % 0.18/0.42 +r3(c, c, b) % 0.18/0.42 +r4(_0) % 0.18/0.42 +r5(_0, _1) % 0.18/0.42 +s0(d) % 0.18/0.42 +s0(b) % 0.18/0.42 -s0(e) % 0.18/0.42 +s1(_0) % 0.18/0.42 +s1(b) % 0.18/0.42 +s2(d) % 0.18/0.42 +s2(e) % 0.18/0.42 +s2(a) % 0.18/0.42 +s2(b) % 0.18/0.42 +s2(c) % 0.18/0.42 +s3(d, _0) % 0.18/0.42 +s3(e, _0) % 0.18/0.42 +s3(a, _0) % 0.18/0.42 +s3(b, _0) % 0.18/0.42 +s3(c, _0) % 0.18/0.42 +s4(d) % 0.18/0.42 +s4(e) % 0.18/0.42 +s4(a) % 0.18/0.42 +s4(b) % 0.18/0.42 +s4(c) % 0.18/0.42 +s5(_0) % 0.18/0.42 SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------