%------------------------------------------------------------------------------ % File : Equinox---6.0.1a % Problem : SYN888-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:short % Command : equinox --modelfile /tmp/model --no-progress --time %d --tstp %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 : 600s % DateTime : Thu Jul 21 05:20:57 EDT 2022 % Result : Satisfiable 24.49s 24.63s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN888-1 : TPTP v8.1.0. Released v2.5.0. % 0.11/0.13 % Command : equinox --modelfile /tmp/model --no-progress --time %d --tstp %s % 0.13/0.34 % Computer : n007.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jul 11 17:47:18 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.34 Equinox, version 6.0.1alpha, 2011-12-07, pre-release. % 0.13/0.34 +++ PROBLEM: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.13/0.34 Reading '/export/starexec/sandbox2/benchmark/theBenchmark.p' ... OK % 0.92/1.18 +++ SOLVING: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.74/1.96 #elt|#instances % 1.81/2.04 (SAT)(equ)(fun)(SAT) 47| -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 2.26/2.44 (SAT)(equ)(fun)(SAT) 47| -. % 2.26/2.44 (SAT)(equ)(fun)(SAT) 47+ -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 2.55/2.73 (SAT)(equ)(fun)(SAT) 47| -. % 2.55/2.73 (SAT)(equ)(fun)(SAT) 47+ -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 2.84/3.03 (SAT)(equ)(fun)(SAT) 47| -. % 2.84/3.03 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 3.14/3.32 (SAT)(equ)(fun)(SAT) 47| -. % 3.14/3.33 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 3.45/3.62 (SAT)(equ)(fun)(SAT) 47| -. % 3.45/3.62 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 3.74/3.92 (SAT)(equ)(fun)(SAT) 47| -. % 3.74/3.92 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 4.05/4.21 (SAT)(equ)(fun)(SAT) 47| -. % 4.05/4.21 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 4.36/4.53 (SAT)(equ)(fun)(SAT) 47| -. -. % 4.36/4.54 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 4.64/4.81 (SAT)(equ)(fun)(SAT) 47| -. -. % 4.64/4.82 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 4.92/5.09 (SAT)(equ)(fun)(SAT) 47| -. -. % 4.92/5.09 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 5.14/5.37 (SAT)(equ)(fun)(SAT) 47| -. -. % 5.14/5.38 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 5.51/5.68 (SAT)(equ)(fun)(SAT) 47| -. -. % 5.53/5.69 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 5.73/5.96 (SAT)(equ)(fun)(SAT) 47| -. -. % 5.73/5.96 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 6.04/6.24 (SAT)(equ)(fun)(SAT) 47| -. -. % 6.04/6.24 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 6.35/6.51 (SAT)(equ)(fun)(SAT) 47| -. -. % 6.35/6.52 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 6.55/6.79 (SAT)(equ)(fun)(SAT) 47| -. % 6.55/6.79 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 6.85/7.09 (SAT)(equ)(fun)(SAT) 47| -. % 6.85/7.09 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 7.14/7.37 (SAT)(equ)(fun)(SAT) 47| -. % 7.14/7.37 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 7.44/7.65 (SAT)(equ)(fun)(SAT) 47| -. % 7.44/7.65 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 7.75/7.93 (SAT)(equ)(fun)(SAT) 47| -. % 7.75/7.93 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 7.96/8.21 (SAT)(equ)(fun)(SAT) 47| -. % 8.05/8.21 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 8.28/8.50 (SAT)(equ)(fun)(SAT) 47| -. % 8.28/8.50 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 8.58/8.78 (SAT)(equ)(fun)(SAT) 47| -. % 8.58/8.79 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 8.87/9.07 (SAT)(equ)(fun)(SAT) 47| -. -. % 8.87/9.07 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 9.17/9.35 (SAT)(equ)(fun)(SAT) 47| -. % 9.17/9.36 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 9.47/9.64 (SAT)(equ)(fun)(SAT) 47| -. -. % 9.47/9.64 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 9.76/9.94 (SAT)(equ)(fun)(SAT) 47| -. -. % 9.76/9.95 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 10.05/10.23 (SAT)(equ)(fun)(SAT) 47| -. -. % 10.05/10.23 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 10.36/10.51 (SAT)(equ)(fun)(SAT) 47| -. -. % 10.36/10.52 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 10.56/10.80 (SAT)(equ)(fun)(SAT) 47| -. -. % 10.56/10.80 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 10.94/11.09 (SAT)(equ)(fun)(SAT) 47| -. -. % 10.94/11.09 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 11.14/11.39 (SAT)(equ)(fun)(SAT) 47| -. % 11.14/11.40 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 11.52/11.68 (SAT)(equ)(fun)(SAT) 47| -. % 11.52/11.68 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 11.74/11.97 (SAT)(equ)(fun)(SAT) 47| -. % 11.74/11.97 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 12.05/12.26 (SAT)(equ)(fun)(SAT) 47| -. % 12.05/12.26 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 12.34/12.56 (SAT)(equ)(fun)(SAT) 47| -. % 12.34/12.57 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 12.63/12.85 (SAT)(equ)(fun)(SAT) 47| -. % 12.63/12.86 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 12.95/13.14 (SAT)(equ)(fun)(SAT) 47| -. % 12.95/13.14 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 13.25/13.43 (SAT)(equ)(fun)(SAT) 47| -. % 13.25/13.43 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 13.56/13.72 (SAT)(equ)(fun)(SAT) 47| -. -. % 13.56/13.73 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 13.85/14.03 (SAT)(equ)(fun)(SAT) 47| -. -. % 13.85/14.04 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 14.17/14.33 (SAT)(equ)(fun)(SAT) 47| -. -. % 14.17/14.34 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 14.44/14.64 (SAT)(equ)(fun)(SAT) 47| -. -. % 14.44/14.65 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 14.74/14.96 (SAT)(equ)(fun)(SAT) 47| -. -. % 14.74/14.97 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 15.14/15.30 (SAT)(equ)(fun)(SAT) 47| -. -. % 15.16/15.31 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 15.45/15.62 (SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. % 15.49/15.64 (SAT)(equ)(fun)(SAT) 47| -. -. -1 % 15.49/15.65 (SAT)(equ)(fun)(SAT) 47| -1 -. -. -. -. -. % 15.49/15.67 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 15.49/15.68 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. % 15.49/15.70 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -. % 15.49/15.71 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -1 -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 15.79/16.00 (SAT)(equ)(fun)(SAT) 47| -1 -1 -. -. -. -. % 15.79/16.02 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -. -. -. % 15.88/16.03 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 16.17/16.33 (SAT)(equ)(fun)(SAT) 47| -. % 16.17/16.33 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 16.47/16.64 (SAT)(equ)(fun)(SAT) 47| -. -. -1 -. -. -. -. -. -. -. -. % 16.47/16.68 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -1 -. -. % 16.55/16.70 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -1 -1 -. -. -. -. % 16.55/16.73 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. % 16.55/16.75 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. % 16.55/16.76 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 % 16.55/16.78 (SAT)(equ)(SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -. -1 % 16.64/16.79 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -. % 16.66/16.80 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 16.94/17.10 (SAT)(equ)(fun)(SAT) 47| -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 16.97/17.19 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. -. % 16.97/17.21 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 16.97/17.21 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 17.07/17.22 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.07/17.22 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. % 17.07/17.24 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.07/17.24 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.07/17.25 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. % 17.07/17.26 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.07/17.27 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 17.07/17.27 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.07/17.28 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. % 17.07/17.30 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. % 17.16/17.31 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.16/17.32 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. % 17.16/17.34 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.16/17.34 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.16/17.35 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.16/17.36 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 17.16/17.37 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.16/17.38 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 17.26/17.43 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 17.26/17.48 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 17.36/17.51 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.36/17.52 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. -. -. -. % 17.36/17.57 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.36/17.58 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 17.36/17.59 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 17.46/17.60 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. % 17.46/17.63 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -1 % 17.46/17.66 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -1 -1 -. -. -. -1 -. -. -. % 17.56/17.70 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -12 -1 -. -. -. -1 -. % 17.56/17.74 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -1 -12 -1 -. -. -. -. % 17.56/17.77 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -1 -. -. % 17.66/17.80 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -1 -. % 17.66/17.83 (SAT)(equ)(SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -1 % 17.66/17.86 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -1 % 17.66/17.88 (SAT)(equ)(SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -. -. -. % 17.76/17.90 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 18.07/18.23 (SAT)(equ)(fun)(SAT) 47| -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 18.16/18.35 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 18.16/18.35 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.16/18.36 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 18.25/18.46 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. -. % 18.25/18.48 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.25/18.48 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 18.35/18.49 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.37/18.52 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. % 18.37/18.53 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.37/18.54 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.37/18.55 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. % 18.37/18.56 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.37/18.57 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 18.37/18.58 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.37/18.59 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. % 18.47/18.61 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 18.47/18.62 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.47/18.63 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. % 18.47/18.65 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.47/18.66 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.47/18.67 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.47/18.68 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 18.47/18.69 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.56/18.70 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 18.56/18.76 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 18.65/18.82 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 18.65/18.83 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.65/18.84 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. % 18.65/18.89 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.76/18.90 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. % 18.77/18.91 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 18.78/18.93 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. % 18.78/18.97 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -1 -. -. -. -. % 18.87/19.01 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -1 -1 -. -. -1 -. -. -. -1 -. % 18.87/19.05 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -12 -1 -. -1 -. -. -. -. -. % 18.94/19.10 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -1 -12 -1 -1 -. -. -. -. % 18.94/19.14 (SAT)(equ)(SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -1 -. -. % 19.03/19.18 (SAT)(equ)(SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -. -. -. -1 -1 -. % 19.08/19.24 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 % 19.08/19.26 (SAT)(equ)(SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -. -1 % 19.08/19.28 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. % 19.08/19.29 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 19.48/19.64 (SAT)(equ)(fun)(SAT) 47| -. % 19.48/19.65 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 19.85/20.00 (SAT)(equ)(fun)(SAT) 47| -. % 19.85/20.01 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -1 -. -. -. -. -. % 20.25/20.38 (SAT)(equ)(fun)(SAT) 47| -. -. -. -. -. -. % 20.25/20.41 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. -. -. -. -. -. % 20.58/20.77 (SAT)(equ)(fun)(SAT) 47| -. % 20.58/20.78 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 -. -. -. % 20.98/21.13 (SAT)(equ)(fun)(SAT) 47| -. -. -1 -12 -. -12 -. -. -. -. -. -. % 20.98/21.19 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -. -. % 21.07/21.22 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 % 21.07/21.24 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -12 -1 -12 % 21.07/21.27 (SAT)(equ)(SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -. -1 -12 % 21.16/21.32 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -. -. % 21.16/21.35 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 % 21.16/21.38 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 % 21.26/21.40 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 % 21.26/21.43 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. % 21.26/21.45 (SAT)(equ)(fun)(SAT) 47| -. -. -1 % 21.26/21.47 (SAT)(equ)(fun)(SAT) 47| -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 21.46/21.61 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -1 % 21.56/21.74 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 21.66/21.88 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 21.77/21.96 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. % 21.77/21.97 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 % 21.77/21.99 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. -. % 21.87/22.01 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. % 21.87/22.05 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 % 21.87/22.07 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. % 21.87/22.09 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. % 21.87/22.11 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. % 21.97/22.12 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 % 21.97/22.14 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. -. -. -. % 21.97/22.17 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. -. -. % 22.07/22.21 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 % 22.07/22.22 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. % 22.07/22.25 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. % 22.07/22.28 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 % 22.15/22.30 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 % 22.15/22.32 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. % 22.15/22.34 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 % 22.15/22.36 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 22.28/22.49 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 22.47/22.60 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 22.55/22.71 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 % 22.55/22.73 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 22.69/22.83 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 22.78/22.93 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. % 22.78/22.96 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 % 22.78/22.98 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 22.85/23.07 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -1 -. -. -. -. -. -. -. -. -. -. -. -. -. -1 % 22.99/23.16 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -12 -. -. -1 -. -. -. -. -. -. -. -1 -. -. -. -. -. % 23.08/23.28 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -1 -12 -1 -. -. -. -. -. -. -. -. -. -. -. -. % 23.15/23.37 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -1 -. -. -. -. -. -. -. -. -. -. -. % 23.30/23.46 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -1 -. -. -. -. -. % 23.39/23.52 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -1 -. -. -. -. % 23.39/23.58 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -1 -. -. -. % 23.46/23.64 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -1 -. -. % 23.54/23.69 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -1 -. -. -. -. -. -. % 23.60/23.76 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -1 % 23.60/23.80 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -12 -1 % 23.69/23.84 (SAT)(equ)(SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -. -12 -1 -. -. % 23.76/23.91 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -12 -1 -. % 23.76/23.95 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -12 -1 % 23.85/23.98 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -12 -. % 23.88/24.02 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -1 % 23.89/24.05 (SAT)(equ)(fun)(SAT) 47| -. -. -1 -. -. -. -. % 23.89/24.10 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 -. -. % 23.98/24.13 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 23.98/24.15 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. -1 % 23.98/24.18 (SAT)(equ)(SAT)(equ)(fun)(SAT) 47| -. % 24.04/24.19 (SAT)(equ)(fun)(SAT) 47+ -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. -. % 24.49/24.63 +++ RESULT: Satisfiable % 24.49/24.63 SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------